From 5fbca6bb29378a846f12759d52a5fb9641f63377 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Sep 2005 15:13:52 +0000
Subject: [PATCH] we have to pass back lastmeta and not newmeta (newmeta <=
 lastmeta). just a cut and paste bug...

---
 helm/ocaml/tactics/proofEngineHelpers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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:
-- 
2.39.2