Generalize ported to the new select up to unification.

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 8bbe05dcb77b1cc78f19e857033aec95e3bee5a2..1f2e6b13c9bd312db7ec309b2d88cf1b045533c2 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -72,7 +72,6 @@ let generalize_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
  pattern
  =
-(*
   let module PET = ProofEngineTypes in
   let generalize_tac mk_fresh_name_callback
        ~pattern:(term,hyps_pat,concl_pat) status
@@ -82,20 +81,31 @@ let generalize_tac
    let module C = Cic in
    let module P = PrimitiveTactics in
    let module T = Tacticals in
-    let _,metasenv,_,_ = proof in
+    let uri,metasenv,pbo,pty = proof in
     let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
-    let selected_hyps,terms_with_context =
-     ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
-    let typ,term =
+    let subst,metasenv,u,selected_hyps,terms_with_context =
+     ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+      ~conjecture ~pattern in
+    let context = CicMetaSubst.apply_subst_context subst context in
+    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
+      | Some term -> Some (CicMetaSubst.apply_subst subst term) in
+    let u,typ,term =
      match terms_with_context, term with
         [], None ->
          raise UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
       | _, Some term
       | (_,term)::_, None ->
-         fst
-          (CicTypeChecker.type_of_aux' metasenv context term
-            CicUniv.empty_ugraph),
-         term in
+         let typ,u =
+          CicTypeChecker.type_of_aux' ~subst metasenv context term u
+         in
+          u,typ,term
+    in
     (* We need to check:
         1. whether they live in the context of the goal;
            if they do they are also well-typed since they are closed subterms
@@ -118,12 +128,12 @@ let generalize_tac
            raise TheSelectedTermsMustLiveInTheGoalContext
         end;
         (* 2 *)
-        let b,u1 = CicReduction.are_convertible context term t u in 
+        let b,u1 = CicReduction.are_convertible ~subst context term t u in 
          if not b then 
           raise AllSelectedTermsMustBeConvertible
          else
           u1
-      ) CicUniv.empty_ugraph terms_with_context) ;
+      ) u terms_with_context) ;
     PET.apply_tactic 
      (T.thens 
        ~start:
@@ -143,5 +153,4 @@ let generalize_tac
        status
  in
   PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
-*) assert false
 ;;