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 23aa20bfb50cb30d4483e5fd2c04400281ce7934..51405f5fdfa7269f58c3b780b16484eb7b67e85d 100644 (file)
--- 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: