* http://cs.unibo.it/helm/.
*)
+open HelmLibraryObjects
let rec injection_tac ~term ~status:((proof, goal) as status) =
let module C = Cic in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
(match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI)
+ or (U.eq equri Logic_Type.eqt_URI) -> (
match tty with
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with (* an equality *)
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI) or
+ (U.eq equri Logic_Type.eqt_URI) -> (
match tty with (* some inductive type *)
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI) or (U.eq equri Logic_Type.eqt_URI) -> (
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((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
- else (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/True.ind"),0,[]))
+ then (C.MutInd(Logic.false_URI,0,[]))
+ else (C.MutInd(Logic.true_URI,0,[]))
in aux red_ty 1
)
constructor_list
let (proof',goals') =
EliminationTactics.elim_type_tac
- ~term:(C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
+ ~term:(C.MutInd(Logic.false_URI,0,[]))
~status
in
(match goals' with