;;
-
-
let print_subst ?(prefix="\n") subst =
String.concat prefix
(List.map
| Eq -> "="
| Incomparable -> "I"
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+
module OrderedTerm =
struct
type t = Cic.term
module IntSet = Set.Make(OrderedInt)
let compute_equality_weight (ty,left,right,o) =
- let factor = 1 in
+ let factor = 2 in
match o with
| Lt ->
let w, m = (weight_of_term
| (m, _, n) when m > 0 && n > 0 ->
Incomparable
| _ -> assert false
-
;;
| Right -> "Right"
;;
+let eq_URI () =
+ match LibraryObjects.eq_URI () with
+ None -> assert false
+ | Some uri -> uri
-let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
-let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
-let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(eq_URI ())
+let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(eq_URI ())
+let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(eq_URI ())
let eq_XURI () =
- let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+ let s = UriManager.string_of_uri (eq_URI ()) in
UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
-let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(eq_URI ())
+
+let metas_of_term t =
+ List.map fst (CicUtil.metas_of_term t)
+;;
+