Bug fixed in generalization: the goals opened by lazy parsing of the

[helm.git] / helm / ocaml / tactics / variousTactics.ml

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 0e43cb1da0d16d5bd62bbfdbfcf2fedb60fdb122..bc7b52200fccd8b99961dd3a80f534b1cc849a4e 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -98,9 +98,11 @@ let generalize_tac
       | Some term ->
           Some (fun context metasenv ugraph -> 
                   let term, metasenv, ugraph = term context metasenv ugraph in
-                  CicMetaSubst.apply_subst subst term, metasenv, ugraph)
+                   CicMetaSubst.apply_subst subst term,
+                    CicMetaSubst.apply_subst_metasenv subst metasenv,
+                    ugraph)
     in
-    let u,typ,term, metasenv =
+    let u,typ,term, metasenv' =
      let context_of_t, (t, metasenv, u) =
       match terms_with_context, term with
          [], None ->
@@ -134,13 +136,12 @@ let generalize_tac
         2. whether they are convertible
     *)
     ignore (
-     (* TASSI: FIXME *)
      List.fold_left
       (fun u (context_of_t,t) ->
         (* 1 *)
-        let t,subst,metasenv' =
+        let t,subst,metasenv'' =
          try
-          CicMetaSubst.delift_rels [] metasenv
+          CicMetaSubst.delift_rels [] metasenv'
            (List.length context_of_t - List.length context) t
          with
           CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
@@ -148,7 +149,7 @@ let generalize_tac
         (*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);
+        assert (metasenv'' = metasenv');
         (* 2 *)
         let b,u1 = CicReduction.are_convertible ~subst context term t u in 
          if not b then 
@@ -156,24 +157,35 @@ let generalize_tac
          else
           u1
       ) u terms_with_context) ;
-    let status = (uri,metasenv,pbo,pty),goal in
-    PET.apply_tactic 
-     (T.thens 
-       ~start:
-         (P.cut_tac 
-          (C.Prod(
-            (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), 
-            typ,
-            (ProofEngineReduction.replace_lifting_csc 1
-              ~equality:(==) 
-              ~what:(List.map snd terms_with_context)
-              ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context)
-              ~where:ty)
-          )))
-       ~continuations:
-         [(P.apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ;
-           T.id_tac])
-       status
+    let status = (uri,metasenv',pbo,pty),goal in
+    let proof,goals =
+     PET.apply_tactic 
+      (T.thens 
+        ~start:
+          (P.cut_tac 
+           (C.Prod(
+             (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), 
+             typ,
+             (ProofEngineReduction.replace_lifting_csc 1
+               ~equality:(==) 
+               ~what:(List.map snd terms_with_context)
+               ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context)
+               ~where:ty)
+           )))
+        ~continuations:
+          [(P.apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ;
+            T.id_tac])
+        status
+    in
+     let _,metasenv'',_,_ = proof in
+      (* CSC: the following is just a bad approximation since a meta
+         can be closed and then re-opened! *)
+      (proof,
+        goals @
+         (List.filter
+           (fun j -> List.exists (fun (i,_,_) -> i = j) metasenv'')
+           (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+             ~newmetasenv:metasenv')))
  in
   PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
 ;;