*)
let equality_is_a_congruence_A =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var"
let equality_is_a_congruence_x =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var"
let equality_is_a_congruence_y =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var"
let apolynomial_uri =
uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
*)
let uri_of_proof ~proof:(uri, _, _, _) = uri
- (**
- @param metano meta list index
- @param metasenv meta list (environment)
- @raise Failure if metano is not found in metasenv
- @return conjecture corresponding to metano in metasenv
- *)
-let conj_of_metano metano =
- try
- List.find (function (m, _, _) -> m = metano)
- with Not_found ->
- failwith (
- "Ring.conj_of_metano: " ^
- (string_of_int metano) ^ " no such meta")
-
(**
@param status current proof engine status
@raise Failure if proof is None
*)
let context_of_status ~status:(proof, goal as status) =
let metasenv = metasenv_of_status ~status:status in
- let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
context
(** CIC TERM CONSTRUCTORS *)
*)
let ringable =
let is_equality = function
- | Cic.MutInd (uri, 0, []) when (eq uri Logic_Type.eqt_URI) -> true
+ | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true
| _ -> false
in
let is_real = function
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
let (_, metasenv, _, _) = proof in
- let (_, context, _) = conj_of_metano goal metasenv in
+ let (_, context, _) = CicUtil.lookup_meta goal metasenv in
let proof',goal' = aux count context status in
assert (goal = goal') ;
proof',[goal']
*)
let ring_tac ~status:((proof, goal) as status) =
warn "in Ring tactic";
- let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in
+ let eqt = mkMutInd (Logic.eq_URI, 0) [] in
let r = Reals.r in
let metasenv = metasenv_of_status ~status in
- let (metano, context, ty) = conj_of_metano goal metasenv in
+ let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
match (build_segments ~terms:[t1; t2]) with
| (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
"exact sym_eqt su t1 ...", exact_tac
~term:(
Cic.Appl
- [mkConst Logic_Type.sym_eqt_URI
+ [mkConst Logic.sym_eq_URI
[equality_is_a_congruence_A, Reals.r;
equality_is_a_congruence_x, t1'' ;
equality_is_a_congruence_y, t1
exact_tac
~term:(
Cic.Appl
- [mkConst Logic_Type.sym_eqt_URI
+ [mkConst Logic.sym_eq_URI
[equality_is_a_congruence_A, Reals.r;
equality_is_a_congruence_x, t2'' ;
equality_is_a_congruence_y, t2