X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=8304d7bb19264738127e76f6409988d69ab14934;hb=da59a744767c799ad287489c55f2ff972f93d93c;hp=7ed946170b5e36e018304c7062a033f96a4cb20c;hpb=f3e1cddb1513c14530f1849477b6f5d0090b88cf;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 7ed946170..8304d7bb1 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -22,8 +22,10 @@
  * For details, see the HELM World-Wide-Web page,
  * http://cs.unibo.it/helm/.
  *)
+
+(* $Id$ *)
  
-let rec rewrite_tac ~direction ~pattern equality =
+let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
  let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
  =
   let module C = Cic in
@@ -35,20 +37,20 @@ let rec rewrite_tac ~direction ~pattern equality =
   assert (wanted = None);   (* this should be checked syntactically *)
   let proof,goal = status in
   let curi, metasenv, pbo, pty = proof in
-  let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
+  let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
   match hyps_pat with
      he::(_::_ as tl) ->
        PET.apply_tactic
         (Tacticals.then_
           (rewrite_tac ~direction
-           ~pattern:(None,[he],Cic.Implicit None) equality)
+           ~pattern:(None,[he],None) equality)
           (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality)
         ) status
-   | [_] as hyps_pat when concl_pat <> Cic.Implicit None ->
+   | [_] as hyps_pat when concl_pat <> None ->
        PET.apply_tactic
         (Tacticals.then_
           (rewrite_tac ~direction
-           ~pattern:(None,hyps_pat,Cic.Implicit None) equality)
+           ~pattern:(None,hyps_pat,None) equality)
           (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality)
         ) status
    | _ ->
@@ -83,11 +85,11 @@ let rec rewrite_tac ~direction ~pattern equality =
                ProofEngineStructuralRules.clearbody name;
                ReductionTactics.change_tac
                 ~pattern:
-                  (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None)
+                  (None,[name,Cic.Implicit (Some `Hole)], None)
                 (ProofEngineTypes.const_lazy_term typ);
                ProofEngineStructuralRules.clear dummy
               ]),
-         pat,gty
+         Some pat,gty
     | _::_ -> assert false
   in
   let if_right_to_left do_not_change a b = 
@@ -130,7 +132,11 @@ let rec rewrite_tac ~direction ~pattern equality =
   let lifted_conjecture =
     metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in
   let lifted_pattern =
-    Some (fun _ m u -> lifted_t1, m, u),[],CicSubstitution.lift 1 concl_pat
+    let lifted_concl_pat =
+      match concl_pat with
+      | None -> None
+      | Some term -> Some (CicSubstitution.lift 1 term) in
+    Some (fun _ m u -> lifted_t1, m, u),[],lifted_concl_pat
   in
   let subst,metasenv',ugraph,_,selected_terms_with_context =
    ProofEngineHelpers.select
@@ -195,8 +201,9 @@ let rewrite_simpl_tac ~direction ~pattern equality =
    ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality)
 ;;
 
-let replace_tac ~pattern ~with_what =
- let replace_tac ~pattern:(wanted,hyps_pat,concl_pat) ~with_what status =
+let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
+ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
+  let _wanted, hyps_pat, concl_pat = pattern in
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -249,7 +256,7 @@ let replace_tac ~pattern ~with_what =
           ty_of_with_what ty_of_t_in_context u in
          if b then
           let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in
-          let pattern_for_t = None,[],concl_pat_for_t in
+          let pattern_for_t = None,[],Some concl_pat_for_t in
            t_in_context,pattern_for_t
          else
           raise
@@ -259,7 +266,7 @@ let replace_tac ~pattern ~with_what =
   let rec aux n whats status =
    match whats with
       [] -> ProofEngineTypes.apply_tactic T.id_tac status
-    | (what,pattern)::tl ->
+    | (what,lazy_pattern)::tl ->
        let what = CicSubstitution.lift n what in
        let with_what = CicSubstitution.lift n with_what in
        let ty_of_with_what = CicSubstitution.lift n ty_of_with_what in
@@ -275,7 +282,7 @@ let replace_tac ~pattern ~with_what =
             ~continuations:[            
               T.then_
                 ~start:(
-                  rewrite_tac ~direction:`LeftToRight ~pattern (C.Rel 1))
+                  rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1))
                  ~continuation:(
                    T.then_
                     ~start:(