New command default "foo" uri1 ... urin

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

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index b86cf43d6048f8efa55cfa00ebabd81e61a006c4..ee76921b23ff0729649bed6030e1fedeffae67a6 100644 (file)
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -37,7 +37,7 @@ let absurd_tac ~term =
     then ProofEngineTypes.apply_tactic 
       (P.apply_tac 
          ~term:(
-           C.Appl [(C.Const (LibraryObjects.absurd_URI , [] )) ; 
+           C.Appl [(C.Const (LibraryObjects.absurd_URI (), [] )) ; 
                   term ; ty])
       ) 
       status
@@ -61,7 +61,7 @@ let contradiction_tac =
            ~start:
              (EliminationTactics.elim_type_tac 
                 ~term:
-                  (C.MutInd (LibraryObjects.false_URI, 0, [])))
+                  (C.MutInd (LibraryObjects.false_URI (), 0, [])))
            ~continuation: VariousTactics.assumption_tac))
     status
    with