X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FnegationTactics.ml;h=65fe892fa61a09aa161226ddc135708ff0a52d21;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=12848ad26eb728e63fba02787e6b330888510031;hpb=f5b6be7239a35e1d0aba504605b5a0df5cf06726;p=helm.git

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index 12848ad26..65fe892fa 100644
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -24,7 +24,8 @@
  *)
 
 
-let absurd_tac ~term ~status:((proof,goal) as status) =
+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
@@ -32,12 +33,12 @@ let absurd_tac ~term ~status:((proof,goal) as status) =
     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 ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
+              ~term:(C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; term ; ty]) status
       else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
 ;;
 
 
-let contradiction_tac ~status =
+let contradiction_tac status =
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
@@ -50,9 +51,9 @@ let contradiction_tac ~status =
            ~start:
              (EliminationTactics.elim_type_tac 
                 ~term:
-                  (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"), 0, [])))
+                  (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, [])))
            ~continuation: VariousTactics.assumption_tac)
-    ~status
+    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 *)
@@ -60,13 +61,13 @@ let contradiction_tac ~status =
 
 (* 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)
 ;;
 *)