From 7efeff178470ab204e531cd07176091bf5022da6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Oct 2014 12:56:43 +0200
Subject: 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.
---
 kernel/indtypes.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 39455a7d2a..45e0261d3c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -666,7 +666,8 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
   let mp, dp, l = repr_mind kn in
   let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
   let ci = 
-    let print_info = { ind_nargs = 0; style = LetStyle } in
+    let print_info =
+      { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
       { ci_ind     = ind;
 	ci_npar    = nparamargs;
 	ci_cstr_ndecls = mind_consnrealdecls;
-- 
cgit v1.2.3