- removed some unneeded dependencies from debian/control

[helm.git] / helm / ocaml / tactics / equalityTactics.ml

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 1c2a7d37fb1a83fc9e15cfc9ec989088a9af57f5..3af6b861dd4ddafc15c18b0e8aff8d43ecba6bc6 100644 (file)
--- 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