Partial porting to V8 URIs.

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

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index 12848ad26eb728e63fba02787e6b330888510031..fc21ec4052e1348be930f66520740d6241d34410 100644 (file)
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -32,7 +32,7 @@ let absurd_tac ~term ~status:((proof,goal) as status) =
     let _,context,ty = CicUtil.lookup_meta goal metasenv in
      if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
       then P.apply_tac 
-              ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
+              ~term:(C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; term ; ty]) ~status
       else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
 ;;
 
@@ -50,7 +50,7 @@ let contradiction_tac ~status =
            ~start:
              (EliminationTactics.elim_type_tac 
                 ~term:
-                  (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"), 0, [])))
+                  (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, [])))
            ~continuation: VariousTactics.assumption_tac)
     ~status
    with