X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=208864c801f1a2fdeafa99506ade65b46f901f51;hb=a772e377c1ca7c43c3e1e25eb47479fc3c5ceb9e;hp=04bfe9ae5e297de46e120cb3dc092826343995d6;hpb=01b776465cd1d0779e635a551da0c6ca77d05b70;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 04bfe9ae5..208864c80 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -584,14 +584,16 @@ let simpl context =
                  aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
                in
                 (**** Step 3 ****)
-                let term_to_fold =
+                let term_to_fold, delta_expanded_term_to_fold =
                  let body' = CicSubstitution.subst_vars exp_named_subst' body in
                   match constant_args with
-                     [] -> body'
-                   | _ -> C.Appl (body'::constant_args)
+                     [] -> C.Const (uri,exp_named_subst'), body'
+                   | _ ->
+                     C.Appl ((C.Const (uri,exp_named_subst'))::constant_args),
+                      C.Appl (body'::constant_args)
                 in
                  let simplified_term_to_fold =
-                  reduceaux context [] term_to_fold
+                  reduceaux context [] delta_expanded_term_to_fold
                  in
                   replace (=) simplified_term_to_fold term_to_fold res
               with