Use unelaborated syntax for ExplainThis

hazelgrove · Dec 27, 2024 · 7158c4a · 7158c4a
1 parent bd36673
commit 7158c4a
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git 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
@@ -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,