X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=51405f5fdfa7269f58c3b780b16484eb7b67e85d;hb=a93a94942ad58d8645af1fd94bef8fa31d9541a4;hp=23aa20bfb50cb30d4483e5fd2c04400281ce7934;hpb=9e3eb63a93acaca0b4ad59c213e9ea430524d3ae;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 23aa20bfb..51405f5fd 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -649,7 +649,7 @@ let saturate_term newmeta metasenv context ty goal_arity =
          in
           if prod_no + 1 = goal_arity then
            let head = CicReduction.normalize ~delta:false context ty in
-            head,[],[],newmeta,goal_arity + 1
+            head,[],[],lastmeta,goal_arity + 1
           else
            (** NORMALIZE RATIONALE 
             * we normalize the target only NOW since we may be in this case: