From 10b525d1f3d4ffd1c95e8a0c3e580a64b0f20c5f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 23 Feb 2006 13:13:04 +0000 Subject: [PATCH] During simplify, reduction of the argument of a Fix and of a MutCase is now performed using simplify. (It used to be performed by whd). Pros: sometimes you should get simpler terms (but not so far) Cons: sometimes simplification could simplify less than expected (but not so far) --- helm/software/components/tactics/proofEngineReduction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml index 1502b600f..db25ae575 100644 --- a/helm/software/components/tactics/proofEngineReduction.ml +++ b/helm/software/components/tactics/proofEngineReduction.ml @@ -701,7 +701,7 @@ let simpl context = reduceaux context tl' body' | t -> t in - (match decofix (CicReduction.whd context term) with + (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = @@ -814,7 +814,7 @@ let simpl context = with _ -> raise AlreadySimplified in - (match CicReduction.whd context recparam with + (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with C.MutConstruct _ | C.Appl ((C.MutConstruct _)::_) -> let body' = -- 2.39.2