diff options
| author | herbelin | 2010-06-03 22:41:28 +0000 |
|---|---|---|
| committer | herbelin | 2010-06-03 22:41:28 +0000 |
| commit | 3f96c12fc3108b3b66f78b3288d29ef26da98ed8 (patch) | |
| tree | 9b016a0799eb891a3f761c63b7ab3349f9dfb5a3 /kernel/inductive.ml | |
| parent | 238309bfddfa68f7a4982afa6a005a8110b0ffb1 (diff) | |
"Improved" the form of the inferred type of "match" by
betaiota-reducing it automatically (this allows for instance to
directly obtain the expected type for "match" expressions that have a
"in I x return match x with ... end" automatically inferred return
predicate feature (see e.g. Vhead and Vtail in Bvector.v).
The need for this "optimization" was not noticed in V8.2 because in
Bvector.v, betaiota was applied peremptorily at the end of sections.
The need for it has been revealed by the removal of reduction at section
closing when Arnaud introduced the new proof engine (should in
particular make CoLoR compile).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13068 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
| -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 e5d73b6e2a..343fae48a3 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -344,7 +344,7 @@ let build_branches_type ind (_,mip as specif) params p = (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) let build_case_type n p c realargs = - betazeta_appvect (n+1) p (Array.of_list (realargs@[c])) + whd_betaiota (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) let type_case_branches env (ind,largs) pj c = let specif = lookup_mind_specif env ind in |