* http://cs.unibo.it/helm/.
*)
-open HelmLibraryObjects
-
let debug_print = fun _ -> ()
let rec injection_tac ~term =
ProofEngineTypes.apply_tactic
(match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri Logic.eq_URI) -> (
+ when LibraryObjects.is_eq_URI equri -> (
match tty with
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
match termty with (* an equality *)
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri Logic.eq_URI) -> (
+ when LibraryObjects.is_eq_URI equri -> (
match tty with (* some inductive type *)
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
| _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct")
in
ProofEngineTypes.apply_tactic
- (P.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1'))
(C.Appl [
C.Lambda (
))
~continuation:
(T.then_
- ~start:(EqualityTactics.rewrite_simpl_tac ~term ())
+ ~start:
+ (EqualityTactics.rewrite_simpl_tac
+ ~direction:`LeftToRight
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ term)
~continuation:EqualityTactics.reflexivity_tac
)
])
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri Logic.eq_URI) -> (
+ when LibraryObjects.is_eq_URI equri -> (
match tty with
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
C.Lambda (binder,source,(aux target (k+1)))
| _ ->
if (id = false_constr_id)
- then (C.MutInd(Logic.false_URI,0,[]))
- else (C.MutInd(Logic.true_URI,0,[]))
+ then (C.MutInd(LibraryObjects.false_URI (),0,[]))
+ else (C.MutInd(LibraryObjects.true_URI (),0,[]))
in aux red_ty 1
)
constructor_list
let (proof',goals') =
ProofEngineTypes.apply_tactic
(EliminationTactics.elim_type_tac
- ~term:(C.MutInd(Logic.false_URI,0,[])))
+ (C.MutInd(LibraryObjects.false_URI (),0,[])))
status
in
(match goals' with
ProofEngineTypes.apply_tactic
(T.then_
~start:
- (P.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
(C.Appl [
C.Lambda (
~continuation:
(
T.then_
- ~start:(EqualityTactics.rewrite_back_simpl_tac
- ~term ())
+ ~start:
+ (EqualityTactics.rewrite_simpl_tac
+ ~direction:`RightToLeft
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ term)
~continuation:(IntroductionTactics.constructor_tac ~n:1)
))
(proof',goal')