From 7b724139a09c5d875131c5861a32d225d5b4b07b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Feb 2019 15:52:30 +0100
Subject: Constructor type information uses the expanded form.

It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.

Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
---
 plugins/extraction/extraction.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 204f889f90..ef6c07bff2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1044,7 +1044,9 @@ let fake_match_projection env p =
   let indu = mkIndU (ind,u) in
   let ctx, paramslet =
     let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
-    let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in
+    let (ctx, cty) = mip.mind_nf_lc.(0) in
+    let cty = Term.it_mkProd_or_LetIn cty ctx in
+    let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in
     List.chop mip.mind_consnrealdecls.(0) rctx
   in
   let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
-- 
cgit v1.2.3