let module P = PrimitiveTactics in
let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
+ let absurd_URI =
+ match LibraryObjects.absurd_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"absurd\" theorem first. Please use the \"default\" command"))
+ 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 (), [] )) ;
+ C.Appl [(C.Const (absurd_URI, [] )) ;
term ; ty])
)
status
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
+ let false_URI =
+ match LibraryObjects.false_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command"))
+ in
try
ProofEngineTypes.apply_tactic (
T.then_
~continuation:(
T.then_
~start:
- (EliminationTactics.elim_type_tac
- (C.MutInd (LibraryObjects.false_URI (), 0, [])))
+ (EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
~continuation: VariousTactics.assumption_tac))
status
with