From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 9 Jul 2005 07:38:59 +0000 (+0000)
Subject: Generalize ported to the new select up to unification.
X-Git-Tag: pre_notation~65
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb19a912c9d3d470163e88722e3abbd548b8bdb9;p=helm.git

Generalize ported to the new select up to unification.
---

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 8bbe05dcb..1f2e6b13c 100644
--- 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
 ;;