* 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 "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 ((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")
(* 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)
;;
*)