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 1502b600f3c6122b4f37f0918bfe7aeb0e2f2384..db25ae575e0aac1a5d706812add3ac1eccd28b2d 100644 (file)
--- 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' =