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/reduction.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index a6ebda491..ced0fd341 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