ocaml 3.09 transition

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

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index 25c29918fc157097b7cd1bf526dd77ff95073889..8f05ae436bc450d4697cf4afc69e652b1db8c2dd 100644 (file)
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -23,50 +23,63 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
-let absurd_tac ~term ~status:((proof,goal) as 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
   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)) (* 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")
+  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)
 ;;
 
-
-let contradiction_tac ~status =
+(* 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
   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 ((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"), 0, [])))
-           ~continuation: VariousTactics.assumption_tac)
-    ~status
+                (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
 ;;
 
 (* Questa era in fourierR.ml
 (* !!!!! fix !!!!!!!!!! *)
-let contradiction_tac ~status:(proof,goal)=
+let contradiction_tac (proof,goal)=
         Tacticals.then_
                 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
                 ~continuation:(Tacticals.then_
                         ~start:(VariousTactics.elim_type_tac ~term:_False)
                         ~continuation:(assumption_tac))
-        ~status:(proof,goal)
+        (proof,goal)
 ;;
 *)