X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=21f2cbebf72aa68f375e204345dbed3a52b717c0;hb=6ab193f88745acd3def85e47d643a92efb2f9fc5;hp=0446132c5163a022c46d5314992768886d72d6e6;hpb=7074f0403d1bec7f4d60715e50a0fe0ef0993567;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 0446132c5..21f2cbebf 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -444,7 +444,7 @@ let reduce context =
         in
          if l = [] then t' else C.Appl (t'::l)
  and reduceaux_exp_named_subst context l =
-  List.map (function uri,t -> uri,reduceaux context l t)
+  List.map (function uri,t -> uri,reduceaux context [] t)
  in
   reduceaux context []
 ;;
@@ -604,11 +604,8 @@ let simpl context =
                    if l = [] then t' else C.Appl (t'::l)
              end
          | C.Constant (_,None,_,_) ->
-            let exp_named_subst' =
-             reduceaux_exp_named_subst context l exp_named_subst
-            in
-             let t' = C.Const (uri,exp_named_subst') in
-              if l = [] then t' else C.Appl (t'::l)
+            let t' = C.Const (uri,exp_named_subst') in
+             if l = [] then t' else C.Appl (t'::l)
          | C.Variable _ -> raise ReferenceToVariable
          | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -739,7 +736,7 @@ let simpl context =
        in
          if l = [] then t' else C.Appl (t'::l)
  and reduceaux_exp_named_subst context l =
-  List.map (function uri,t -> uri,reduceaux context l t)
+  List.map (function uri,t -> uri,reduceaux context [] t)
  in
   reduceaux context []
 ;;