From 7158c4a32c106d1cb527d08bd5c94d0a9b4e1183 Mon Sep 17 00:00:00 2001
From: Alexander Bandukwala <7h3kk1d@gmail.com>
Date: Fri, 27 Dec 2024 14:58:06 -0500
Subject: [PATCH] Use unelaborated syntax for ExplainThis

---
 src/haz3lcore/statics/Info.re    | 10 ++++++++++
 src/haz3lweb/view/ExplainThis.re |  1 +
 2 files changed, 11 insertions(+)

diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re
index 593c1550f4..94b181c6a4 100644
--- a/src/haz3lcore/statics/Info.re
+++ b/src/haz3lcore/statics/Info.re
@@ -797,3 +797,13 @@ let typ_is_constructor_expected = t =>
   | {expects: ConstructorExpected(_) | VariantExpected(_), _} => true
   | _ => false
   };
+
+let rec unelaborated_info = (info: t): t =>
+  switch (info) {
+  | InfoExp({unelaborated_info: ui, _}) =>
+    switch (ui) {
+    | Some(info) => unelaborated_info(InfoExp(info))
+    | None => info
+    }
+  | _ => info
+  };
diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re
index e508bb2eb2..5879480b8b 100644
--- a/src/haz3lweb/view/ExplainThis.re
+++ b/src/haz3lweb/view/ExplainThis.re
@@ -2496,6 +2496,7 @@ let view =
       ~explainThisModel: ExplainThisModel.t,
       info: option(Info.t),
     ) => {
+  let info = Option.map(Info.unelaborated_info, info);
   let (syn_form, (explanation, _), example) =
     get_doc(
       ~docs=explainThisModel,