more work on matitaprover (no more XML and buris are created).

[helm.git] / helm / software / components / tactics / proofEngineReduction.ml

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index db25ae575e0aac1a5d706812add3ac1eccd28b2d..6d198d4d133e721539c30e77d86196787ff6c1b5 100644 (file)
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/components/tactics/proofEngineReduction.ml
@@ -595,12 +595,24 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ (* a simplified term is active if it can create a redex when used as an *)
+ (* actual parameter                                                     *)
+ let rec is_active =
+  function
+     C.Lambda _
+   | C.MutConstruct _
+   | C.Appl (C.MutConstruct _::_)
+   | C.CoFix _ -> true
+   | C.Cast (bo,_) -> is_active bo
+   | C.LetIn _ -> assert false
+   | _ -> false
+ in
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
  let rec reduceaux context l =
-  let module C = Cic in
-  let module S = CicSubstitution in
    function
       C.Rel n as t ->
        (* we never perform delta expansion automatically *)
@@ -653,9 +665,13 @@ let simpl context =
         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
          match o with
            C.Constant (_,Some body,_,_,_) ->
-            try_delta_expansion context l
-             (C.Const (uri,exp_named_subst'))
-             (CicSubstitution.subst_vars exp_named_subst' body)
+            if List.exists is_active l then
+             try_delta_expansion context l
+              (C.Const (uri,exp_named_subst'))
+              (CicSubstitution.subst_vars exp_named_subst' body)
+            else
+             let t' = C.Const (uri,exp_named_subst') in
+              if l = [] then t' else C.Appl (t'::l)
          | C.Constant (_,None,_,_,_) ->
             let t' = C.Const (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)
@@ -843,7 +859,7 @@ let simpl context =
       let simplified_term_to_fold =
        reduceaux context [] delta_expanded_term_to_fold
       in
-       replace (=) [simplified_term_to_fold] [term_to_fold] res
+       replace_lifting (=) [simplified_term_to_fold] [term_to_fold] res
    with
       WrongShape ->
        (**** Step 3.2 ****)