let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
- 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 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")
+ 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)
+ ProofEngineTypes.mk_tactic (absurd_tac ~term)
;;
let contradiction_tac =
~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