X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=bc6d522b983171aa0adc1ad8018b7d34eb46acbf;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=8bbe05dcb77b1cc78f19e857033aec95e3bee5a2;hpb=bf40c378bd2c624405be2118a478a0734eb8d3aa;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 8bbe05dcb..bc6d522b9 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,43 @@ 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 =
-     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 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 =
+     let context_of_t,t =
+      match terms_with_context, term with
+         [], None ->
+          raise
+           UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
+       | _, Some t -> context,t
+       | (context_of_t,t)::_, None -> context_of_t,t
+     in
+      let t,subst,metasenv' =
+       try
+        CicMetaSubst.delift_rels [] metasenv
+         (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
+    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
@@ -108,22 +130,24 @@ let generalize_tac
      List.fold_left
       (fun u (context_of_t,t) ->
         (* 1 *)
-        begin
+        let t,subst,metasenv' =
          try
-          ignore
-           (CicMetaSubst.delift_rels [] metasenv
-             (List.length context_of_t - List.length context) t)
+          CicMetaSubst.delift_rels [] metasenv
+           (List.length context_of_t - List.length context) t
          with
           CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-           raise TheSelectedTermsMustLiveInTheGoalContext
-        end;
+           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);
         (* 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 +167,4 @@ let generalize_tac
        status
  in
   PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
-*) assert false
 ;;