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

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index 0e3c0c142..8f05ae436 100644
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -41,12 +41,12 @@ let absurd_tac ~term =
 	           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? *)
+(* 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
@@ -65,7 +65,7 @@ let contradiction_tac =
            ~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