From 1388171a48d8e068d5d0ed93b74faa4ac7da5f7f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 14:23:02 +0100
Subject: Fixing typo resulting in wrong printing of return clauses for
 inductive types with let-in in arity.

---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index adf714db35..356a699c66 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -273,7 +273,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let ind_tags =
-    rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in
+    rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
   let cstr_tags =
     Array.map2 (fun c n ->
       let d,_ = decompose_prod_assum c in
-- 
cgit v1.2.3


From b286c9f4f42febfd37f9715d81eaf118ab24aa94 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 16:29:28 +0100
Subject: Add support so that the type of a match in an inductive type with
 let-in is reduced as if without let-in, when applied to arguments.

This allows e.g. to have a head-betazeta-reduced goal in the following example.

Inductive Foo : let X := Set in X := I : Foo.
Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 356a699c66..7f6a4a6442 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -526,7 +526,7 @@ let type_case_branches_with_names env indspec p c =
   let (params,realargs) = List.chop nparams args in
   let lbrty = Inductive.build_branches_type ind specif params p in
   (* Build case type *)
-  let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
+  let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env p (ind,params) then
     (set_pattern_names env (fst ind) lbrty, conclty)
-- 
cgit v1.2.3