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/nativecode.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 041751ecfe..c8a4fa897c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1807,7 +1807,7 @@ let compile_constant env sigma prefix ~interactive con cb =
       let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; 
 		 ci_cstr_nargs = [|0|];
 		 ci_cstr_ndecls = [||] (*FIXME*);
-		 ci_pp_info = { ind_nargs = 0; style = RegularStyle } } in
+		 ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in
       let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci;
 		  asw_reloc = tbl; asw_finite = true } in
       let c_uid = fresh_lname Anonymous in
-- 
cgit v1.2.3