intersect uris siguris
let compare_goal_list proof goal1 goal2 =
- let _,metasenv,_,_ = proof in
+ let _,metasenv, _subst, _,_, _ = proof in
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ =
let cmatch' = Constr.cmatch'
(* used only by te old auto *)
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
- let (_, metasenv, _, _) = proof in
+let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
let set = signature_of_hypothesis context metasenv in
close_with_types set metasenv context
-let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
+let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let ty_set = Constr.constants_of ty in
let hyp_set = signature_of_hypothesis context metasenv in
let uris =
Constr.UriManagerSet.fold
(fun u acc ->
- prerr_endline ("processing "^(UriManager.string_of_uri u));
+ debug_print (lazy ("processing "^(UriManager.string_of_uri u)));
let set_for_sigmatch =
Constr.UriManagerSet.remove u all_constants_closed in
if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
(* equality has a special treatment *)
- (prerr_endline "special treatment";
+ (debug_print (lazy "special treatment");
let tfe =
Constr.SetSet.elements (types_for_equality metasenv goal)
in
List.fold_left
(fun acc l ->
let tyl = Constr.UriManagerSet.elements l in
- prerr_endline ("tyl: "^(String.concat "\n"
- (List.map UriManager.string_of_uri tyl)));
+ debug_print (lazy ("tyl: "^(String.concat "\n"
+ (List.map UriManager.string_of_uri tyl))));
let set_for_sigmatch =
Constr.UriManagerSet.diff set_for_sigmatch l in
let uris =
acc @ uris)
acc tfe)
else
- (prerr_endline "normal treatment";
+ (debug_print (lazy "normal treatment");
let uris =
sigmatch ~dbd ~facts:false ~where:`Statement
(Some (u,[]),set_for_sigmatch)
Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set
;;
-let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
+let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
(*
let to_string set =
"{\n" ^
^ "\n}"
in
*)
- let (_, metasenv, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants =
match signature with
(* else raise Goal_is_not_an_equation *)
let experimental_hint
- ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
- let (_, metasenv, _, _) = proof in
+ ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with
(aux uris)
let new_experimental_hint
- ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
+ ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
((proof, goal) as status)
=
- let (_, metasenv, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with