Bug fixed in generalize: a status was generated with an old metasenv.

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index fc6413eb5ceb385d0056f9d6b978e8679216ac2c..0e43cb1da0d16d5bd62bbfdbfcf2fedb60fdb122 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -92,7 +92,6 @@ let generalize_tac
     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
     let pbo = CicMetaSubst.apply_subst subst pbo in
     let pty = CicMetaSubst.apply_subst subst pty in
-    let status = (uri,metasenv,pbo,pty),goal in
     let term =
      match term with
         None -> None
@@ -118,13 +117,14 @@ let generalize_tac
          (List.length context_of_t - List.length context) t
        with
         CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-         raise TheSelectedTermsMustLiveInTheGoalContext in
-      (*CSC: I am not sure about the following two assertions;
-        maybe I need to propagate the new subst and metasenv *)
-      assert (subst = []);
-      assert (metasenv' = metasenv);
-      let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in
-       u,typ,t,metasenv
+         raise TheSelectedTermsMustLiveInTheGoalContext
+      in
+       (*CSC: I am not sure about the following two assertions;
+         maybe I need to propagate the new subst and metasenv *)
+       assert (subst = []);
+       assert (metasenv' = metasenv);
+       let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in
+        u,typ,t,metasenv
     in
     (* We need to check:
         1. whether they live in the context of the goal;
@@ -156,6 +156,7 @@ let generalize_tac
          else
           u1
       ) u terms_with_context) ;
+    let status = (uri,metasenv,pbo,pty),goal in
     PET.apply_tactic 
      (T.thens 
        ~start: