diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-27 16:29:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-27 16:59:29 +0100 |
| commit | b286c9f4f42febfd37f9715d81eaf118ab24aa94 (patch) | |
| tree | 77a696ea6d4de8d7b160f05c1c26c9aeff6448a7 /kernel | |
| 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 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6b4dd536a..ca814f497 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -364,7 +364,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in vargs @ [dep_cstr] in - let base = beta_appvect (lift nargs p) (Array.of_list cargs) in + let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base args in Array.mapi build_one_branch mip.mind_nf_lc |