From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 23 Feb 2006 13:13:04 +0000 (+0000)
Subject: During simplify, reduction of the argument of a Fix and of a MutCase is now
X-Git-Tag: make_still_working~7533
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10b525d1f3d4ffd1c95e8a0c3e580a64b0f20c5f;p=helm.git

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)
---

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' =