A patch for printing "match" when constructors are defined with let-in

but the internal representation dropped let-in.

Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.

To do, there is still an extra @ in the constructor name that does not
need to be there.

1 files changed, 8 insertions, 1 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 91072dce8..70c670e3f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -273,7 +273,14 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let print_info = { ind_nargs = mip.mind_nrealdecls; style = style } in
+  let ind_tags =
+    rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in
+  let cstr_tags =
+    Array.map2 (fun c n ->
+      let d,_ = decompose_prod_assum c in
+      rel_context_tags (List.firstn n d))
+      mip.mind_nf_lc mip.mind_consnrealdecls in
+  let print_info = { ind_tags; cstr_tags; style } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
     ci_cstr_ndecls = mip.mind_consnrealdecls;