Added Decompose tactic

[helm.git] / helm / gTopLevel / negationTactics.ml

diff --git a/helm/gTopLevel/negationTactics.ml b/helm/gTopLevel/negationTactics.ml
index d55f04556cb249cfb52d89f76f779c837e006522..2b87bb911d7ebc28160cb147318ea9e72b6839c9 100644 (file)
--- a/helm/gTopLevel/negationTactics.ml
+++ b/helm/gTopLevel/negationTactics.ml
@@ -30,7 +30,7 @@ let absurd_tac ~term ~status:((proof,goal) as status) =
   let module P = PrimitiveTactics in
    let _,metasenv,_,_ = proof in
     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-     if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop))
+     if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
       then P.apply_tac 
               ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
       else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
@@ -42,7 +42,8 @@ let contradiction_tac ~status =
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
-   T.then_
+   try
+    T.then_
       ~start: P.intros_tac
       ~continuation:(
         T.then_
@@ -50,6 +51,9 @@ let contradiction_tac ~status =
                      ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ))
            ~continuation: VariousTactics.assumption_tac)
     ~status
+   with 
+    (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption")
+    (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
 ;;
 
 (* Questa era in fourierR.ml