+ List.map snd
+ (MetadataConstraints.sigmatch ~dbd ~facts ~where:`Statement signature)
+ in
+ intersect uris siguris
+
+let compare_goal_list proof goal1 goal2 =
+ let _,metasenv,_,_ = proof in
+ let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
+ let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
+ let ty_sort1,_ =
+ CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph
+ in
+ let ty_sort2,_ =
+ CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph
+ in
+ let prop1 =
+ let b,_ =
+ CicReduction.are_convertible
+ ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph
+ in
+ if b then 0
+ else 1
+ in
+ let prop2 =
+ let b,_ =
+ CicReduction.are_convertible
+ ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph
+ in
+ if b then 0
+ else 1
+ in
+ prop1 - prop2
+
+let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+ let (_, metasenv, _, _) = proof in
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let (uris, (main, sig_constants)) =
+ match signature with
+ | Some signature -> (Constr.sigmatch ~dbd ~facts signature, signature)
+ | None -> (Constr.cmatch' ~dbd ~facts ty, Constr.signature_of ty)
+ in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ let types_constants =
+ match main with
+ | None -> Constr.StringSet.empty
+ | Some (main, types) ->
+ List.fold_right Constr.StringSet.add (main :: types)
+ Constr.StringSet.empty
+ in
+ let hyp_constants =
+ Constr.StringSet.diff (signature_of_hypothesis context) types_constants