X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=3af6b861dd4ddafc15c18b0e8aff8d43ecba6bc6;hb=7cb90c67bc6f8113188a91ecc29f6db20db5aeb8;hp=1c2a7d37fb1a83fc9e15cfc9ec989088a9af57f5;hpb=0583c44e19ee683efab796bf21904bbfc64fbf1e;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 1c2a7d37f..3af6b861d 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -61,9 +61,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
       C.Lambda
        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
     in
-    let fresh_meta = ProofEngineHelpers.new_meta proof in
-    let irl =
-     ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+    let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 
      let (proof',goals) =
@@ -123,9 +122,9 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
       C.Lambda
        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
     in
-    let fresh_meta = ProofEngineHelpers.new_meta proof in
+    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
     let irl =
-     ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+     CicMkImplicit.identity_relocation_list_for_metavariable context in
     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 
      let (proof',goals) =
@@ -164,6 +163,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
          match CicTypeChecker.type_of_aux' metasenv context wty with
             C.Sort C.Set -> "cic:/Coq/Init/Logic/eq.ind"
           | C.Sort C.Type
+	  | C.Sort C.CProp
           | C.Sort C.Prop -> "cic:/Coq/Init/Logic_Type/eqT.ind"
           | _ -> assert false
         in