From 3f96c12fc3108b3b66f78b3288d29ef26da98ed8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 3 Jun 2010 22:41:28 +0000
Subject: "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
---
 kernel/inductive.ml  | 2 +-
 kernel/reduction.ml  | 3 +++
 kernel/reduction.mli | 1 +
 3 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel')

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
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index e215f23361..e8fea82800 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -94,6 +94,9 @@ let pure_stack lfts stk =
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
 
+let whd_betaiota t =
+  whd_val (create_clos_infos betaiota empty_env) (inject t)
+
 let nf_betaiota t =
   norm_val (create_clos_infos betaiota empty_env) (inject t)
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index a6ebda4918..ced0fd3413 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -17,6 +17,7 @@ val whd_betaiotazeta        : constr -> constr
 val whd_betadeltaiota       : env -> constr -> constr
 val whd_betadeltaiota_nolet : env -> constr -> constr
 
+val whd_betaiota      : constr -> constr
 val nf_betaiota      : constr -> constr
 
 (***********************************************************************
-- 
cgit v1.2.3