X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineReduction.ml;h=1db075c70d96455a80c15ab49865eb3a02cde7be;hb=30da02e8be0612dac41b435bc7e8a9bea41cc352;hp=db25ae575e0aac1a5d706812add3ac1eccd28b2d;hpb=2f4481184300cd4ffd3072555872f369ec8a008e;p=helm.git

diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml
index db25ae575..1db075c70 100644
--- a/components/tactics/proofEngineReduction.ml
+++ b/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)