name specifications added for elim_intros, elim_intros_simpl and elim_type

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

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index c8c9785dae9cdfe094c7c7fed6d543fbb9b3aed6..0e3c0c142180a9f5570233f4a03528780711224c 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 (HelmLibraryObjects.Logic.absurd_URI , [] )) ; 
+           C.Appl [(C.Const (LibraryObjects.absurd_URI (), [] )) ; 
                   term ; ty])
       ) 
       status
@@ -46,6 +46,7 @@ let absurd_tac ~term =
    ProofEngineTypes.mk_tactic (absurd_tac ~term)
 ;;
 
+(* FG: METTERE I NOMI ANCHE QUI? *)
 let contradiction_tac =
  let contradiction_tac status =
   let module C = Cic in
@@ -60,8 +61,7 @@ let contradiction_tac =
         T.then_
            ~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