From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Sep 2005 15:13:52 +0000 (+0000)
Subject: we have to pass back lastmeta and not newmeta (newmeta <= lastmeta).
X-Git-Tag: V_0_1_2_1~11
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5fbca6bb29378a846f12759d52a5fb9641f63377;p=helm.git

we have to pass back lastmeta and not newmeta (newmeta <= lastmeta).
just a cut and paste bug...
---

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: