diff options
| author | Hugo Herbelin | 2015-02-27 16:29:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-27 16:59:29 +0100 |
| commit | b286c9f4f42febfd37f9715d81eaf118ab24aa94 (patch) | |
| tree | 77a696ea6d4de8d7b160f05c1c26c9aeff6448a7 /pretyping/inductiveops.ml | |
| parent | 5f8c0bfbb04de58a527d373c3994592e5853d4e2 (diff) | |
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. *)
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |