aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml14
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/decls.ml13
-rw-r--r--library/global.mli6
-rw-r--r--library/globnames.ml23
-rw-r--r--library/globnames.mli8
-rw-r--r--library/goptions.ml15
-rw-r--r--library/heads.ml11
-rw-r--r--library/impargs.ml15
-rw-r--r--library/keys.ml28
-rw-r--r--library/lib.ml9
-rw-r--r--library/lib.mli8
-rw-r--r--library/libnames.ml4
-rw-r--r--library/libobject.ml12
-rw-r--r--library/libobject.mli5
-rw-r--r--library/library.ml56
-rw-r--r--library/library.mli3
-rw-r--r--library/loadpath.ml27
-rw-r--r--library/loadpath.mli2
-rw-r--r--library/nameops.ml4
-rw-r--r--library/nametab.ml8
-rw-r--r--library/summary.ml15
-rw-r--r--library/summary.mli4
-rw-r--r--library/universes.ml83
-rw-r--r--library/universes.mli13
25 files changed, 194 insertions, 194 deletions
diff --git a/library/declare.ml b/library/declare.ml
index c9d5fdbe2..b0df32b8d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -398,7 +398,7 @@ let declare_mind mie =
let pr_rank i = pr_nth (i+1)
let fixpoint_message indexes l =
- Flags.if_verbose msg_info (match l with
+ Flags.if_verbose Feedback.msg_info (match l with
| [] -> anomaly (Pp.str "no recursive definition")
| [id] -> pr_id id ++ str " is recursively defined" ++
(match indexes with
@@ -413,7 +413,7 @@ let fixpoint_message indexes l =
| None -> mt ()))
let cofixpoint_message l =
- Flags.if_verbose msg_info (match l with
+ Flags.if_verbose Feedback.msg_info (match l with
| [] -> anomaly (Pp.str "No corecursive definition.")
| [id] -> pr_id id ++ str " is corecursively defined"
| l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
@@ -423,16 +423,16 @@ let recursive_message isfix i l =
(if isfix then fixpoint_message i else cofixpoint_message) l
let definition_message id =
- Flags.if_verbose msg_info (pr_id id ++ str " is defined")
+ Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
let assumption_message id =
- Flags.if_verbose msg_info (pr_id id ++ str " is assumed")
+ (* Changing "assumed" to "declared", "assuming" referring more to
+ the type of the object than to the name of the object (see
+ discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
+ Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
(** Global universe names, in a different summary *)
-type universe_names =
- (Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
-
(* Discharged or not *)
type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b3858146d..f3f734aa0 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -371,7 +371,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 =
match idl, objs0 with
| _,[] -> []
| id::idl,(id',obj)::tail when Id.equal id id' ->
- assert (object_has_tag obj "MODULE");
+ assert (String.equal (object_tag obj) "MODULE");
let mp_id = MPdot(mp0, Label.of_id id) in
let objs = match idl with
| [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1
diff --git a/library/decls.ml b/library/decls.ml
index 0cd4ccb25..6e21880f1 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -11,7 +11,6 @@
open Util
open Names
-open Context
open Decl_kinds
open Libnames
@@ -47,16 +46,20 @@ let constant_kind kn = Cmap.find kn !csttab
(** Miscellaneous functions. *)
+open Context.Named.Declaration
+
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
List.fold_right
- (fun (id,c,t as d) signv ->
- let d = if variable_opacity id then (id,None,t) else d in
+ (fun d signv ->
+ let id = get_id d in
+ let d = if variable_opacity id then LocalAssum (id, get_type d) else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
let last_section_hyps dir =
- fold_named_context
- (fun (id,_,_) sec_ids ->
+ Context.Named.fold_outside
+ (fun d sec_ids ->
+ let id = get_id d in
try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
with Not_found -> sec_ids)
(Environ.named_context (Global.env()))
diff --git a/library/global.mli b/library/global.mli
index 9db30c8ff..bf653307c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -19,9 +19,9 @@ val env : unit -> Environ.env
val env_is_initial : unit -> bool
-val universes : unit -> Univ.universes
+val universes : unit -> UGraph.t
val named_context_val : unit -> Environ.named_context_val
-val named_context : unit -> Context.named_context
+val named_context : unit -> Context.Named.t
(** {6 Enriching the global environment } *)
@@ -73,7 +73,7 @@ val add_module_parameter :
(** {6 Queries in the global environment } *)
-val lookup_named : variable -> Context.named_declaration
+val lookup_named : variable -> Context.Named.Declaration.t
val lookup_constant : constant -> Declarations.constant_body
val lookup_inductive : inductive ->
Declarations.mutual_inductive_body * Declarations.one_inductive_body
diff --git a/library/globnames.ml b/library/globnames.ml
index 3ae44b2cc..bec463ecf 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -14,10 +14,10 @@ open Libnames
(*s Global reference is a kernel side type for all references together *)
type global_reference =
- | VarRef of variable
- | ConstRef of constant
- | IndRef of inductive
- | ConstructRef of constructor
+ | VarRef of variable (** A reference to the section-context. *)
+ | ConstRef of constant (** A reference to the environment. *)
+ | IndRef of inductive (** A reference to an inductive type. *)
+ | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
let isVarRef = function VarRef _ -> true | _ -> false
let isConstRef = function ConstRef _ -> true | _ -> false
@@ -107,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y =
let global_ord_gen ord_cst ord_ind ord_cons x y =
if x == y then 0
else match x, y with
+ | VarRef v1, VarRef v2 -> Id.compare v1 v2
+ | VarRef _, _ -> -1
+ | _, VarRef _ -> 1
| ConstRef cx, ConstRef cy -> ord_cst cx cy
+ | ConstRef _, _ -> -1
+ | _, ConstRef _ -> 1
| IndRef indx, IndRef indy -> ord_ind indx indy
+ | IndRef _, _ -> -1
+ | _ , IndRef _ -> 1
| ConstructRef consx, ConstructRef consy -> ord_cons consx consy
- | VarRef v1, VarRef v2 -> Id.compare v1 v2
-
- | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1
- | ConstRef _, VarRef _ -> 1
- | ConstRef _, (IndRef _ | ConstructRef _) -> -1
- | IndRef _, (VarRef _ | ConstRef _) -> 1
- | IndRef _, ConstructRef _ -> -1
- | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1
let global_hash_gen hash_cst hash_ind hash_cons gr =
let open Hashset.Combine in
diff --git a/library/globnames.mli b/library/globnames.mli
index f94f6216f..f4956e3df 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -13,10 +13,10 @@ open Mod_subst
(** {6 Global reference is a kernel side type for all references together } *)
type global_reference =
- | VarRef of variable
- | ConstRef of constant
- | IndRef of inductive
- | ConstructRef of constructor
+ | VarRef of variable (** A reference to the section-context. *)
+ | ConstRef of constant (** A reference to the environment. *)
+ | IndRef of inductive (** A reference to an inductive type. *)
+ | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
val isVarRef : global_reference -> bool
val isConstRef : global_reference -> bool
diff --git a/library/goptions.ml b/library/goptions.ml
index 5f6512e11..4aa3a2a21 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -108,7 +108,8 @@ module MakeTable =
(fun c -> t := MySet.remove c !t))
let print_table table_name printer table =
- pp (str table_name ++
+ Feedback.msg_notice
+ (str table_name ++
(hov 0
(if MySet.is_empty table then str " None" ++ fnl ()
else MySet.fold
@@ -122,7 +123,7 @@ module MakeTable =
method mem x =
let y = A.encode x in
let answer = MySet.mem y !t in
- msg_info (A.member_message y answer)
+ Feedback.msg_info (A.member_message y answer)
method print = print_table A.title A.printer !t
end
@@ -271,7 +272,7 @@ let declare_option cast uncast
in
let warn () =
if depr then
- msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
+ Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
in
let cread () = cast (read ()) in
let cwrite v = warn (); write (uncast v) in
@@ -346,12 +347,12 @@ let set_int_option_value_gen locality =
set_option_value locality check_int_value
let set_bool_option_value_gen locality key v =
try set_option_value locality check_bool_value key v
- with UserError (_,s) -> msg_warning s
+ with UserError (_,s) -> Feedback.msg_warning s
let set_string_option_value_gen locality =
set_option_value locality check_string_value
let unset_option_value_gen locality key =
try set_option_value locality check_unset_value key ()
- with UserError (_,s) -> msg_warning s
+ with UserError (_,s) -> Feedback.msg_warning s
let set_int_option_value = set_int_option_value_gen None
let set_bool_option_value = set_bool_option_value_gen None
@@ -375,9 +376,9 @@ let print_option_value key =
let s = read () in
match s with
| BoolValue b ->
- msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+ Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
| _ ->
- msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+ Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
let get_tables () =
let tables = !value_tab in
diff --git a/library/heads.ml b/library/heads.ml
index 8124d3474..4c9b78976 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -15,6 +15,7 @@ open Environ
open Globnames
open Libobject
open Lib
+open Context.Named.Declaration
(** Characterization of the head of a term *)
@@ -63,9 +64,9 @@ let kind_of_head env t =
(try on_subterm k l b (variable_head id)
with Not_found ->
(* a goal variable *)
- match pi2 (lookup_named id env) with
- | Some c -> aux k l c b
- | None -> NotImmediatelyComputableHead)
+ match lookup_named id env with
+ | LocalDef (_,c,_) -> aux k l c b
+ | LocalAssum _ -> NotImmediatelyComputableHead)
| Const (cst,_) ->
(try on_subterm k l b (constant_head cst)
with Not_found ->
@@ -132,8 +133,8 @@ let compute_head = function
| None -> RigidHead (RigidParameter cst)
| Some c -> kind_of_head env c)
| EvalVarRef id ->
- (match pi2 (Global.lookup_named id) with
- | Some c when not (Decls.variable_opacity id) ->
+ (match Global.lookup_named id with
+ | LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
kind_of_head (Global.env()) c
| _ ->
RigidHead (RigidVar id))
diff --git a/library/impargs.ml b/library/impargs.ml
index f5f6a3eba..4e344a954 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -165,6 +165,7 @@ let update pos rig (na,st) =
(* modified is_rigid_reference with a truncated env *)
let is_flexible_reference env bound depth f =
+ let open Context.Named.Declaration in
match kind_of_term f with
| Rel n when n >= bound+depth -> (* inductive type *) false
| Rel n when n >= depth -> (* previous argument *) true
@@ -173,8 +174,7 @@ let is_flexible_reference env bound depth f =
let cb = Environ.lookup_constant kn env in
(match cb.const_body with Def _ -> true | _ -> false)
| Var id ->
- let (_, value, _) = Environ.lookup_named id env in
- begin match value with None -> false | _ -> true end
+ Environ.lookup_named id env |> is_local_def
| Ind _ | Construct _ -> false
| _ -> true
@@ -234,13 +234,14 @@ let find_displayed_name_in all avoid na (_,b as envnames_b) =
let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let rigid = ref true in
+ let open Context.Rel.Declaration in
let rec aux env avoid n names t =
let t = whd_betadeltaiota env t in
match kind_of_term t with
| Prod (na,a,b) ->
let na',avoid' = find_displayed_name_in all avoid na (names,b) in
add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
- (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
+ (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b)
| _ ->
rigid := is_rigid_head t;
let names = List.rev names in
@@ -252,7 +253,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
match kind_of_term (whd_betadeltaiota env t) with
| Prod (na,a,b) ->
let na',avoid = find_displayed_name_in all [] na ([],b) in
- let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
+ let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
!rigid, Array.to_list v
| _ -> true, []
@@ -427,7 +428,7 @@ let compute_mib_implicits flags manual kn =
(Array.mapi (* No need to lift, arities contain no de Bruijn *)
(fun i mip ->
(** No need to care about constraints here *)
- (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i))))
+ Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i))))
mib.mind_packets) in
let env_ar = push_rel_context ar env in
let imps_one_inductive i mip =
@@ -449,8 +450,8 @@ let compute_all_mib_implicits flags manual kn =
let compute_var_implicits flags manual id =
let env = Global.env () in
- let (_,_,ty) = lookup_named id env in
- compute_semi_auto_implicits env flags manual ty
+ let open Context.Named.Declaration in
+ compute_semi_auto_implicits env flags manual (get_type (lookup_named id env))
(* Implicits of a global reference. *)
diff --git a/library/keys.ml b/library/keys.ml
index 0c167494e..057dc3b65 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -12,35 +12,31 @@ open Globnames
open Term
open Libobject
-type key =
+type key =
| KGlob of global_reference
- | KLam
+ | KLam
| KLet
| KProd
| KSort
- | KEvar
- | KCase
- | KFix
+ | KCase
+ | KFix
| KCoFix
- | KRel
- | KMeta
+ | KRel
module KeyOrdered = struct
type t = key
let hash gr =
match gr with
- | KGlob gr -> 10 + RefOrdered.hash gr
+ | KGlob gr -> 8 + RefOrdered.hash gr
| KLam -> 0
| KLet -> 1
| KProd -> 2
| KSort -> 3
- | KEvar -> 4
- | KCase -> 5
- | KFix -> 6
- | KCoFix -> 7
- | KRel -> 8
- | KMeta -> 9
+ | KCase -> 4
+ | KFix -> 5
+ | KCoFix -> 6
+ | KRel -> 7
let compare gr1 gr2 =
match gr1, gr2 with
@@ -62,8 +58,6 @@ module Keyset = Keymap.Set
(* Mapping structure for references to be considered equivalent *)
-type keys = Keyset.t Keymap.t
-
let keys = Summary.ref Keymap.empty ~name:"Keys_decl"
let add_kv k v m =
@@ -153,12 +147,10 @@ let pr_key pr_global = function
| KLet -> str"Let"
| KProd -> str"Product"
| KSort -> str"Sort"
- | KEvar -> str"Evar"
| KCase -> str"Case"
| KFix -> str"Fix"
| KCoFix -> str"CoFix"
| KRel -> str"Rel"
- | KMeta -> str"Meta"
let pr_keyset pr_global v =
prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
diff --git a/library/lib.ml b/library/lib.ml
index e4617cafb..f8bb6bac5 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -428,8 +428,10 @@ let add_section_context ctx =
sectab := (Context ctx :: vars,repl,abs)::sl
let extract_hyps (secs,ohyps) =
+ let open Context.Named.Declaration in
let rec aux = function
- | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
+ | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) ->
+ let (id',b,t) = to_tuple decl in
let l, r = aux (idl,hyps) in
(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
| (Variable (_,_,poly,ctx)::idl,hyps) ->
@@ -448,7 +450,10 @@ let instance_from_variable_context sign =
| [] -> [] in
Array.of_list (inst_rec sign)
-let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx
+let named_of_variable_context ctx = let open Context.Named.Declaration in
+ List.map (function id,_,None,t -> LocalAssum (id,t)
+ | id,_,Some b,t -> LocalDef (id,b,t))
+ ctx
let add_section_replacement f g poly hyps =
match !sectab with
diff --git a/library/lib.mli b/library/lib.mli
index 513c48549..e2e71ac90 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -168,7 +168,7 @@ type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
val instance_from_variable_context : variable_context -> Names.Id.t array
-val named_of_variable_context : variable_context -> Context.named_context
+val named_of_variable_context : variable_context -> Context.Named.t
val section_segment_of_constant : Names.constant -> abstr_info
val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
@@ -179,9 +179,9 @@ val is_in_section : Globnames.global_reference -> bool
val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
val add_section_context : Univ.universe_context_set -> unit
val add_section_constant : Decl_kinds.polymorphic ->
- Names.constant -> Context.named_context -> unit
+ Names.constant -> Context.Named.t -> unit
val add_section_kn : Decl_kinds.polymorphic ->
- Names.mutual_inductive -> Context.named_context -> unit
+ Names.mutual_inductive -> Context.Named.t -> unit
val replacement_context : unit -> Opaqueproof.work_list
(** {6 Discharge: decrease the section level if in the current section } *)
@@ -194,6 +194,6 @@ val discharge_inductive : Names.inductive -> Names.inductive
(* discharging a constant in one go *)
val full_replacement_context : unit -> Opaqueproof.work_list list
val full_section_segment_of_constant :
- Names.constant -> (Context.named_context -> Context.named_context) list
+ Names.constant -> (Context.Named.t -> Context.Named.t) list
diff --git a/library/libnames.ml b/library/libnames.ml
index a2f22b2ef..99ff2f2fb 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -13,7 +13,7 @@ open Names
(**********************************************)
-let pr_dirpath sl = (str (DirPath.to_string sl))
+let pr_dirpath sl = str (DirPath.to_string sl)
(*s Operations on dirpaths *)
@@ -197,7 +197,7 @@ let string_of_reference = function
let pr_reference = function
| Qualid (_,qid) -> pr_qualid qid
- | Ident (_,id) -> str (Id.to_string id)
+ | Ident (_,id) -> Id.print id
let loc_of_reference = function
| Qualid (loc,qid) -> loc
diff --git a/library/libobject.ml b/library/libobject.ml
index 706e39915..b12d2038a 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -8,6 +8,9 @@
open Libnames
open Pp
+open Util
+
+module Dyn = Dyn.Make(struct end)
(* The relax flag is used to make it possible to load files while ignoring
failures to incorporate some objects. This can be useful when one
@@ -70,15 +73,14 @@ type dynamic_object_declaration = {
dyn_discharge_function : object_name * obj -> obj option;
dyn_rebuild_function : obj -> obj }
-let object_tag = Dyn.tag
-let object_has_tag = Dyn.has_tag
+let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
let cache_tab =
(Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
let declare_object_full odecl =
let na = odecl.object_name in
- let (infun,outfun) = Dyn.create na in
+ let (infun, outfun) = Dyn.Easy.make_dyn na in
let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj)
and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj)
and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj)
@@ -131,7 +133,7 @@ let apply_dyn_fun deflt f lobj =
Failure "local to_apply_dyn_fun" ->
if not (!relax_flag || Hashtbl.mem missing_tab tag) then
begin
- Pp.msg_warning
+ Feedback.msg_warning
(Pp.str ("Cannot find library functions for an object with tag "
^ tag ^ " (a plugin may be missing)"));
Hashtbl.add missing_tab tag ()
@@ -158,3 +160,5 @@ let discharge_object ((_,lobj) as node) =
let rebuild_object lobj =
apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
+
+let dump = Dyn.dump
diff --git a/library/libobject.mli b/library/libobject.mli
index f3880a437..dbe0de8f8 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -99,7 +99,6 @@ val declare_object :
'a object_declaration -> ('a -> obj)
val object_tag : obj -> string
-val object_has_tag : obj -> string -> bool
val cache_object : object_name * obj -> unit
val load_object : int -> object_name * obj -> unit
@@ -109,3 +108,7 @@ val classify_object : obj -> obj substitutivity
val discharge_object : object_name * obj -> obj option
val rebuild_object : obj -> obj
val relax : bool -> unit
+
+(** {6 Debug} *)
+
+val dump : unit -> (int * string) list
diff --git a/library/library.ml b/library/library.ml
index e34d38d15..4d0082850 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -132,7 +132,7 @@ let try_find_library dir =
try find_library dir
with Not_found ->
errorlabstrm "Library.find_library"
- (str "Unknown library " ++ str (DirPath.to_string dir))
+ (str "Unknown library " ++ pr_dirpath dir)
let register_library_filename dir f =
(* Not synchronized: overwrite the previous binding if one existed *)
@@ -285,28 +285,18 @@ let locate_absolute_library dir =
with Not_found -> [] in
match find ".vo" @ find ".vio" with
| [] -> raise LibNotFound
- | [file] -> dir, file
+ | [file] -> file
| [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+ Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
str vo ++ str " because it is more recent");
- dir, vi
- | [vo;vi] -> dir, vo
+ vi
+ | [vo;vi] -> vo
| _ -> assert false
let locate_qualified_library ?root ?(warn = true) qid =
(* Search library in loadpath *)
let dir, base = repr_qualid qid in
- let loadpath = match root with
- | None -> Loadpath.expand_path dir
- | Some root ->
- let filter path =
- if is_dirpath_prefix_of root path then
- let path = drop_dirpath_prefix root path in
- is_dirpath_suffix_of dir path
- else false
- in
- Loadpath.filter_path filter
- in
+ let loadpath = Loadpath.expand_path ?root dir in
let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
let find ext =
try
@@ -321,7 +311,7 @@ let locate_qualified_library ?root ?(warn = true) qid =
| [lpath, file] -> lpath, file
| [lpath_vo, vo; lpath_vi, vi]
when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+ Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
str vo ++ str " because it is more recent");
lpath_vi, vi
| [lpath_vo, vo; _ ] -> lpath_vo, vo
@@ -380,7 +370,7 @@ let access_table what tables dp i =
| Fetched t -> t
| ToFetch f ->
let dir_path = Names.DirPath.to_string dp in
- Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+ Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
let t =
try fetch_delayed f
with Faulty f ->
@@ -458,7 +448,7 @@ let intern_from_file f =
module DPMap = Map.Make(DirPath)
let rec intern_library (needed, contents) (dir, f) from =
- Pp.feedback(Feedback.FileDependency (from, f));
+ Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, (needed, contents)
with Not_found ->
@@ -466,13 +456,14 @@ let rec intern_library (needed, contents) (dir, f) from =
try (DPMap.find dir contents).library_digests, (needed, contents)
with Not_found ->
(* [dir] is an absolute name which matches [f] which must be in loadpath *)
+ let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
let m = intern_from_file f in
if not (DirPath.equal dir m.library_name) then
errorlabstrm "load_physical_library"
(str "The file " ++ str f ++ str " contains library" ++ spc () ++
pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
spc() ++ pr_dirpath dir);
- Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
+ Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
and intern_library_deps libs dir m from =
@@ -480,13 +471,13 @@ and intern_library_deps libs dir m from =
(dir :: needed, DPMap.add dir m contents )
and intern_mandatory_library caller from libs (dir,d) =
- let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
+ let digest, libs = intern_library libs (dir, None) from in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
- errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir));
+ errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir);
libs
-let rec_intern_library libs mref =
- let _, libs = intern_library libs mref None in
+let rec_intern_library libs (dir, f) =
+ let _, libs = intern_library libs (dir, Some f) None in
libs
let native_name_from_filename f =
@@ -578,7 +569,7 @@ let safe_locate_module (loc,qid) =
try Nametab.locate_module qid
with Not_found ->
user_err_loc
- (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module")
+ (loc,"import_library", pr_qualid qid ++ str " is not a module")
let import_module export modl =
(* Optimization: libraries in a raw in the list are imported
@@ -603,7 +594,7 @@ let import_module export modl =
try Declaremods.import_module export mp; aux [] l
with Not_found ->
user_err_loc (loc,"import_library",
- str (string_of_qualid dir) ++ str " is not a module"))
+ pr_qualid dir ++ str " is not a module"))
| [] -> flush acc
in aux [] modl
@@ -613,9 +604,9 @@ let import_module export modl =
let check_coq_overwriting p id =
let l = DirPath.repr p in
let is_empty = match l with [] -> true | _ -> false in
- if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
+ if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
errorlabstrm ""
- (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++
+ (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
(* Verifies that a string starts by a letter and do not contain
@@ -764,7 +755,7 @@ let save_library_to ?todo dir f otab =
error "Could not compile the library to native code."
with reraise ->
let reraise = Errors.push reraise in
- let () = msg_warning (str "Removed file " ++ str f') in
+ let () = Feedback.msg_warning (str "Removed file " ++ str f') in
let () = close_out ch in
let () = Sys.remove f' in
iraise reraise
@@ -780,13 +771,6 @@ let save_library_raw f sum lib univs proofs =
System.marshal_out_segment f' ch (proofs : seg_proofs);
close_out ch
-(************************************************************************)
-(*s Display the memory use of a library. *)
-
-open Printf
-
-let mem s = Pp.mt ()
-
module StringOrd = struct type t = string let compare = String.compare end
module StringSet = Set.Make(StringOrd)
diff --git a/library/library.mli b/library/library.mli
index 25c9604ce..8f5b775d8 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -85,8 +85,5 @@ val locate_qualified_library :
*)
-(** {6 Statistics: display the memory use of a library. } *)
-val mem : DirPath.t -> Pp.std_ppcmds
-
(** {6 Native compiler. } *)
val native_name_from_filename : string -> string
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 78f8dd25f..33c0f41e1 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -72,7 +72,7 @@ let add_load_path phys_path coq_path ~implicit =
let () =
(* Do not warn when overriding the default "-I ." path *)
if not (DirPath.equal old_path Nameops.default_root_prefix) then
- msg_warning
+ Feedback.msg_warning
(str phys_path ++ strbrk " was previously bound to " ++
pr_dirpath old_path ++ strbrk "; it is remapped to " ++
pr_dirpath coq_path) in
@@ -84,10 +84,6 @@ let add_load_path phys_path coq_path ~implicit =
end
| _ -> anomaly_too_many_paths phys_path
-let extend_path_with_dirpath p dir =
- List.fold_left Filename.concat p
- (List.rev_map Id.to_string (DirPath.repr dir))
-
let filter_path f =
let rec aux = function
| [] -> []
@@ -97,18 +93,19 @@ let filter_path f =
in
aux !load_paths
-let expand_path dir =
+let expand_path ?root dir =
let rec aux = function
| [] -> []
- | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l ->
- match implicit with
- | true ->
- (** The path is implicit, so that we only want match the logical suffix *)
- if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l
- | false ->
- (** Otherwise we must match exactly *)
- if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
- in
+ | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l ->
+ let success =
+ match root with
+ | None ->
+ if implicit then is_dirpath_suffix_of dir lg
+ else DirPath.equal dir lg
+ | Some root ->
+ is_dirpath_prefix_of root lg &&
+ is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in
+ if success then (ph, lg) :: aux l else aux l in
aux !load_paths
let locate_file fname =
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 49ffc1148..4e79edbdc 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -42,7 +42,7 @@ val find_load_path : CUnix.physical_path -> t
val is_in_load_paths : CUnix.physical_path -> bool
(** Whether a physical path is currently bound. *)
-val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
+val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list
(** Given a relative logical path, associate the list of absolute physical and
logical paths which are possible matches of it. *)
diff --git a/library/nameops.ml b/library/nameops.ml
index 98b417c2a..71405d024 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -12,7 +12,7 @@ open Names
(* Identifiers *)
-let pr_id id = str (Id.to_string id)
+let pr_id id = Id.print id
let pr_name = function
| Anonymous -> str "_"
@@ -141,7 +141,7 @@ let name_max na1 na2 =
| Name _ -> na1
| Anonymous -> na2
-let pr_lab l = str (Label.to_string l)
+let pr_lab l = Label.print l
let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/nametab.ml b/library/nametab.ml
index 40acb3ae2..db902d625 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -119,7 +119,7 @@ struct
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
- msg_warning (str ("Trying to mask the absolute name \""
+ Feedback.msg_warning (str ("Trying to mask the absolute name \""
^ U.to_string n ^ "\"!"));
tree.path
| Nothing
@@ -155,7 +155,7 @@ let rec push_exactly uname o level tree = function
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
- msg_warning (str ("Trying to mask the absolute name \""
+ Feedback.msg_warning (str ("Trying to mask the absolute name \""
^ U.to_string n ^ "\"!"));
tree.path
| Nothing
@@ -523,9 +523,9 @@ let shortest_qualid_of_tactic kn =
KnTab.shortest_qualid Id.Set.empty sp !the_tactictab
let pr_global_env env ref =
- try str (string_of_qualid (shortest_qualid_of_global env ref))
+ try pr_qualid (shortest_qualid_of_global env ref)
with Not_found as e ->
- if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
+ if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
let global_inductive r =
match global r with
diff --git a/library/summary.ml b/library/summary.ml
index 46c52acc4..edea7dbe5 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -10,6 +10,8 @@ open Pp
open Errors
open Util
+module Dyn = Dyn.Make(struct end)
+
type marshallable = [ `Yes | `No | `Shallow ]
type 'a summary_declaration = {
freeze_function : marshallable -> 'a;
@@ -21,7 +23,7 @@ let summaries = ref Int.Map.empty
let mangle id = id ^ "-SUMMARY"
let internal_declare_summary hash sumname sdecl =
- let (infun, outfun) = Dyn.create (mangle sumname) in
+ let (infun, outfun) = Dyn.Easy.make_dyn (mangle sumname) in
let dyn_freeze b = infun (sdecl.freeze_function b)
and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
and dyn_init = sdecl.init_function in
@@ -164,8 +166,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids =
List.filter (fun (id, _) -> List.mem id ids) summaries
let pointer_equal l1 l2 =
+ let ptr_equal d1 d2 =
+ let Dyn.Dyn (t1, x1) = d1 in
+ let Dyn.Dyn (t2, x2) = d2 in
+ match Dyn.eq t1 t2 with
+ | None -> false
+ | Some Refl -> x1 == x2
+ in
CList.for_all2eq
- (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2
+ (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
(** All-in-one reference declaration + registration *)
@@ -176,3 +185,5 @@ let ref ?(freeze=fun _ r -> r) ~name x =
unfreeze_function = ((:=) r);
init_function = (fun () -> r := x) };
r
+
+let dump = Dyn.dump
diff --git a/library/summary.mli b/library/summary.mli
index c24a0b4b8..27889cab2 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -71,3 +71,7 @@ val unfreeze_summary : frozen_bits -> unit
val surgery_summary : frozen -> frozen_bits -> frozen
val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
val pointer_equal : frozen_bits -> frozen_bits -> bool
+
+(** {6 Debug} *)
+
+val dump : unit -> (int * string) list
diff --git a/library/universes.ml b/library/universes.ml
index 3bebdafc7..c4eb2afcb 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -102,6 +102,7 @@ module Constraints = struct
end
type universe_constraints = Constraints.t
+type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
type 'a universe_constrained = 'a * universe_constraints
type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
@@ -135,82 +136,76 @@ let to_constraints g s =
| _, ULe, Some l' -> enforce_leq x y acc
| _, ULub, _ -> acc
| _, d, _ ->
- let f = if d == ULe then check_leq else check_eq in
+ let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in
if f g x y then acc else
raise (Invalid_argument
"to_constraints: non-trivial algebraic constraint between universes")
in Constraints.fold tr s Constraint.empty
-let eq_constr_univs_infer univs m n =
- if m == n then true, Constraints.empty
+let eq_constr_univs_infer univs fold m n accu =
+ if m == n then Some accu
else
- let cstrs = ref Constraints.empty in
- let eq_universes strict = Univ.Instance.check_eq univs in
+ let cstrs = ref accu in
+ let eq_universes strict = UGraph.check_eq_instances univs in
let eq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_eq univs u1 u2 then true
- else
- (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
- true)
+ match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+ | None -> false
+ | Some accu -> cstrs := accu; true
in
let rec eq_constr' m n =
m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
in
let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
- res, !cstrs
+ if res then Some !cstrs else None
(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
to expose subterms of [m] and [n], arguments. *)
-let eq_constr_univs_infer_with kind1 kind2 univs m n =
+let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
(* spiwack: duplicates the code of [eq_constr_univs_infer] because I
haven't find a way to factor the code without destroying
pointer-equality optimisations in [eq_constr_univs_infer].
Pointer equality is not sufficient to ensure equality up to
[kind1,kind2], because [kind1] and [kind2] may be different,
typically evaluating [m] and [n] in different evar maps. *)
- let cstrs = ref Constraints.empty in
- let eq_universes strict = Univ.Instance.check_eq univs in
+ let cstrs = ref accu in
+ let eq_universes strict = UGraph.check_eq_instances univs in
let eq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_eq univs u1 u2 then true
- else
- (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
- true)
+ match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+ | None -> false
+ | Some accu -> cstrs := accu; true
in
let rec eq_constr' m n =
Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
in
let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
- res, !cstrs
+ if res then Some !cstrs else None
-let leq_constr_univs_infer univs m n =
- if m == n then true, Constraints.empty
+let leq_constr_univs_infer univs fold m n accu =
+ if m == n then Some accu
else
- let cstrs = ref Constraints.empty in
- let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in
+ let cstrs = ref accu in
+ let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
let eq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_eq univs u1 u2 then true
- else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
- true)
+ match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+ | None -> false
+ | Some accu -> cstrs := accu; true
in
let leq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_leq univs u1 u2 then
- ((if Univ.is_type0_univ u1 then
- cstrs := Constraints.add (u1, ULe, u2) !cstrs);
- true)
- else
- (cstrs := Constraints.add (u1, ULe, u2) !cstrs;
- true)
+ match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with
+ | None -> false
+ | Some accu -> cstrs := accu; true
in
let rec eq_constr' m n =
m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -220,7 +215,7 @@ let leq_constr_univs_infer univs m n =
eq_constr' leq_constr' m n
and leq_constr' m n = m == n || compare_leq m n in
let res = compare_leq m n in
- res, !cstrs
+ if res then Some !cstrs else None
let eq_constr_universes m n =
if m == n then true, Constraints.empty
@@ -650,14 +645,14 @@ let normalize_univ_variable_opt_subst ectx =
in
let update l b =
assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
- ectx := Univ.LMap.add l (Some b) !ectx; b
+ try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false
in normalize_univ_variable ~find ~update
let normalize_univ_variable_subst subst =
let find l = Univ.LMap.find l !subst in
let update l b =
assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
- subst := Univ.LMap.add l b !subst; b in
+ try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in
normalize_univ_variable ~find ~update
let normalize_universe_opt_subst subst =
@@ -869,27 +864,27 @@ let normalize_context_set ctx us algs =
let csts =
(* We first put constraints in a normal-form: all self-loops are collapsed
to equalities. *)
- let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g)
- ctx Univ.empty_universes
+ let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
+ ctx UGraph.empty_universes
in
let g =
Univ.Constraint.fold
(fun (l, d, r) g ->
let g =
if not (Level.is_small l || LSet.mem l ctx) then
- try Univ.add_universe l false g
- with Univ.AlreadyDeclared -> g
+ try UGraph.add_universe l false g
+ with UGraph.AlreadyDeclared -> g
else g
in
let g =
if not (Level.is_small r || LSet.mem r ctx) then
- try Univ.add_universe r false g
- with Univ.AlreadyDeclared -> g
+ try UGraph.add_universe r false g
+ with UGraph.AlreadyDeclared -> g
else g
in g) csts g
in
- let g = Univ.Constraint.fold Univ.enforce_constraint csts g in
- Univ.constraints_of_universes g
+ let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in
+ UGraph.constraints_of_universes g
in
let noneqs =
Constraint.fold (fun (l,d,r as cstr) noneqs ->
@@ -1027,7 +1022,7 @@ let refresh_constraints univs (ctx, cstrs) =
Univ.Constraint.fold (fun c (cstrs', univs as acc) ->
let c = translate_cstr c in
if is_trivial_leq c then acc
- else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
+ else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
cstrs (Univ.Constraint.empty, univs)
in ((ctx, cstrs'), univs')
diff --git a/library/universes.mli b/library/universes.mli
index edb06dfc5..53cf5f384 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -63,6 +63,7 @@ module Constraints : sig
end
type universe_constraints = Constraints.t
+type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
type 'a universe_constrained = 'a * universe_constraints
type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
@@ -71,11 +72,12 @@ val subst_univs_universe_constraints : universe_subst_fn ->
val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
-val to_constraints : universes -> universe_constraints -> constraints
+val to_constraints : UGraph.t -> universe_constraints -> constraints
(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
application grouping, the universe constraints in [u] and additional constraints [c]. *)
-val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
+ constr -> constr -> 'a -> 'a option
(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
{!eq_constr_univs_infer} taking kind-of-term functions, to expose
@@ -83,12 +85,13 @@ val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_
val eq_constr_univs_infer_with :
(constr -> (constr,types) kind_of_term) ->
(constr -> (constr,types) kind_of_term) ->
- Univ.universes -> constr -> constr -> bool universe_constrained
+ UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
modulo alpha, casts, application grouping, the universe constraints
in [u] and additional constraints [c]. *)
-val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
+ constr -> constr -> 'a -> 'a option
(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
application grouping and the universe constraints in [c]. *)
@@ -223,7 +226,7 @@ val restrict_universe_context : universe_context_set -> universe_set -> universe
val simplify_universe_context : universe_context_set ->
universe_context_set * universe_level_subst
-val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes
+val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t
(** Pretty-printing *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 04:10:20 +0000