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

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index c8c9785da..7ee79e534 100644
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 let absurd_tac ~term =
  let absurd_tac ~term status =
   let (proof, goal) = status in
@@ -37,15 +39,16 @@ 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
-    else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
+    else raise (ProofEngineTypes.Fail (lazy "Absurd: Not a Proposition"))
  in
    ProofEngineTypes.mk_tactic (absurd_tac ~term)
 ;;
 
+(* FG: METTERE I NOMI ANCHE QUI? CSC: in teoria si', per la intros*)
 let contradiction_tac =
  let contradiction_tac status =
   let module C = Cic in
@@ -60,12 +63,11 @@ 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 
-    (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption")
+    ProofEngineTypes.Fail msg when Lazy.force msg = "Assumption: No such assumption" -> raise (ProofEngineTypes.Fail (lazy "Contradiction: No such assumption"))
     (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
  in 
   ProofEngineTypes.mk_tactic contradiction_tac