new universes implementation

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

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index 65fe892fa61a09aa161226ddc135708ff0a52d21..a4b7d9ba844c8868bea0ecc973107b71e67c493d 100644 (file)
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -23,8 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
-let absurd_tac ~term status =
+let absurd_tac ~term =
+ let absurd_tac ~term status =
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -32,31 +32,41 @@ let absurd_tac ~term status =
    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 P.apply_tac 
-              ~term:(C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; term ; ty]) status
+      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")
+ in
+  ProofEngineTypes.mk_tactic (absurd_tac ~term)
 ;;
 
-
-let contradiction_tac status =
+let contradiction_tac =
+ let contradiction_tac status =
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    try
-    T.then_
+    ProofEngineTypes.apply_tactic (
+     T.then_
       ~start:(P.intros_tac ())
       ~continuation:(
-        T.then_
+        T.then_
            ~start:
              (EliminationTactics.elim_type_tac 
                 ~term:
                   (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, [])))
-           ~continuation: VariousTactics.assumption_tac)
+           ~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 *)
+ in 
+  ProofEngineTypes.mk_tactic contradiction_tac
 ;;
 
 (* Questa era in fourierR.ml