X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FequalityTactics.ml;h=69466c272a458ad4c49386ae69b5dad8895ed13a;hb=ce800b0b7acf3940cad3afc5b1d2296155affb1c;hp=da7f599a9ec2b642291173c3d0c6c1d4a6fc5bf6;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml
index da7f599a9..69466c272 100644
--- a/components/tactics/equalityTactics.ml
+++ b/components/tactics/equalityTactics.ml
@@ -80,7 +80,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
                 ~pattern:
                   (None,[name,Cic.Implicit (Some `Hole)], None)
                 (ProofEngineTypes.const_lazy_term typ);
-               ProofEngineStructuralRules.clear dummy
+               ProofEngineStructuralRules.clear [dummy]
               ]),
          Some pat,gty
     | _::_ -> assert false
@@ -145,6 +145,9 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
     selected_terms_with_context ([],[]) in
   let t1 = CicMetaSubst.apply_subst subst t1 in
   let t2 = CicMetaSubst.apply_subst subst t2 in
+  let ty = CicMetaSubst.apply_subst subst ty in
+  let pbo = CicMetaSubst.apply_subst subst pbo in
+  let pty = CicMetaSubst.apply_subst subst pty in
   let equality = CicMetaSubst.apply_subst subst equality in
   let abstr_gty =
    ProofEngineReduction.replace_lifting_csc 0
@@ -205,6 +208,11 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   let uri,metasenv,pbo,pty = proof in
   let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   assert (hyps_pat = []); (*CSC: not implemented yet *)
+  let eq_URI =
+   match LibraryObjects.eq_URI () with
+      Some uri -> uri
+    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
+  in
   let context_len = List.length context in
   let subst,metasenv,u,_,selected_terms_with_context =
    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
@@ -268,7 +276,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
             ~start:(
               P.cut_tac 
                (C.Appl [
-                 (C.MutInd (LibraryObjects.eq_URI (), 0, [])) ;
+                 (C.MutInd (eq_URI, 0, [])) ;
                  ty_of_with_what ; 
                  what ; 
                  with_what]))
@@ -283,15 +291,15 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
                        (function ((proof,goal) as status) ->
                          let _,metasenv,_,_ = proof in
                          let _,context,_ = CicUtil.lookup_meta goal metasenv in
-                         let hyp =
+                         let hyps =
                           try
                            match List.hd context with
-                              Some (Cic.Name name,_) -> name
+                              Some (Cic.Name name,_) -> [name]
                             | _ -> assert false
                           with (Failure "hd") -> assert false
                          in
                           ProofEngineTypes.apply_tactic
-                           (ProofEngineStructuralRules.clear ~hyp) status))
+                           (ProofEngineStructuralRules.clear ~hyps) status))
                     ~continuation:(aux_tac (n + 1) tl));
               T.id_tac])
          status