X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FnegationTactics.ml;h=8f05ae436bc450d4697cf4afc69e652b1db8c2dd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a4b7d9ba844c8868bea0ecc973107b71e67c493d;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index a4b7d9ba8..8f05ae436 100644
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -29,21 +29,24 @@ let absurd_tac ~term =
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
-   let _,metasenv,_,_ = proof in
-    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 ProofEngineTypes.apply_tactic 
-       (P.apply_tac 
-        ~term:(
-         C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; 
-	         term ; ty])
-	) 
-       status
-      else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
+  let _,metasenv,_,_ = proof in
+  let _,context,ty = CicUtil.lookup_meta goal metasenv in
+  let ty_term,_ = 
+    CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+    if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
+    then ProofEngineTypes.apply_tactic 
+      (P.apply_tac 
+         ~term:(
+           C.Appl [(C.Const (LibraryObjects.absurd_URI (), [] )) ; 
+	           term ; ty])
+      ) 
+      status
+    else raise (ProofEngineTypes.Fail (lazy "Absurd: Not a Proposition"))
  in
-  ProofEngineTypes.mk_tactic (absurd_tac ~term)
+   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
@@ -58,12 +61,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