X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FnegationTactics.ml;h=b86cf43d6048f8efa55cfa00ebabd81e61a006c4;hb=b8ac0d11d5cd4083838a3848fce68683a518b54a;hp=c8c9785dae9cdfe094c7c7fed6d543fbb9b3aed6;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index c8c9785da..b86cf43d6 100644
--- 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 (HelmLibraryObjects.Logic.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 (HelmLibraryObjects.Logic.false_URI, 0, [])))
+                  (C.MutInd (LibraryObjects.false_URI, 0, [])))
            ~continuation: VariousTactics.assumption_tac))
     status
    with