* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let absurd_tac ~term =
let absurd_tac ~term status =
let (proof, goal) = status in
then ProofEngineTypes.apply_tactic
(P.apply_tac
~term:(
- C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ;
+ C.Appl [(C.Const (LibraryObjects.absurd_URI (), [] )) ;
term ; ty])
)
status
- else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
+ else raise (ProofEngineTypes.Fail (lazy "Absurd: Not a Proposition"))
in
ProofEngineTypes.mk_tactic (absurd_tac ~term)
;;
+(* 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
T.then_
~start:
(EliminationTactics.elim_type_tac
- ~term:
- (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, [])))
+ (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