From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/uGraph.mli | 76 ++++++++++++++++++++++++++++++++-----------------------
 1 file changed, 45 insertions(+), 31 deletions(-)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e95cf4d1..0f078255 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -1,39 +1,34 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Univ
 
 (** {6 Graphs of universes. } *)
-
 type t
-
 type universes = t
+[@@ocaml.deprecated "Use UGraph.t"]
 
-type 'a check_function = universes -> 'a -> 'a -> bool
-val check_leq : universe check_function
-val check_eq : universe check_function
+type 'a check_function = t -> 'a -> 'a -> bool
 
-(** The empty graph of universes *)
-val empty_universes : universes
+val check_leq : Universe.t check_function
+val check_eq : Universe.t check_function
+val check_eq_level : Level.t check_function
 
 (** The initial graph of universes: Prop < Set *)
-val initial_universes : universes
+val initial_universes : t
 
-val is_initial_universes : universes -> bool
-
-val sort_universes : universes -> universes
-
-(** Adds a universe to the graph, ensuring it is >= or > Set.
-   @raises AlreadyDeclared if the level is already declared in the graph. *)
+(** Check if we are in the initial case *)
+val is_initial_universes : t -> bool
 
-exception AlreadyDeclared
-
-val add_universe : universe_level -> bool -> universes -> universes
+(** Check equality of instances w.r.t. a universe graph *)
+val check_eq_instances : Instance.t check_function
 
 (** {6 ... } *)
 (** Merge of constraints in a universes graph.
@@ -41,23 +36,42 @@ val add_universe : universe_level -> bool -> universes -> universes
   universes graph. It raises the exception [UniverseInconsistency] if the
   constraints are not satisfiable. *)
 
-val enforce_constraint : univ_constraint -> universes -> universes
-val merge_constraints : constraints -> universes -> universes
+val enforce_constraint : univ_constraint -> t -> t
+val merge_constraints : Constraint.t -> t -> t
 
-val constraints_of_universes : universes -> constraints
+val check_constraint  : t -> univ_constraint -> bool
+val check_constraints : Constraint.t -> t -> bool
 
-val check_constraint  : universes -> univ_constraint -> bool
-val check_constraints : constraints -> universes -> bool
+(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *)
+val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
 
-val check_eq_instances : Instance.t check_function
-(** Check equality of instances w.r.t. a universe graph *)
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+   @raise AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : Level.t -> bool -> t -> t
 
 (** {6 Pretty-printing of universes. } *)
 
-val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
+val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t
+
+(** The empty graph of universes *)
+val empty_universes : t
+[@@ocaml.deprecated "Use UGraph.initial_universes"]
+
+val sort_universes : t -> t
+
+val constraints_of_universes : t -> Constraint.t
+
+val check_subtype : AUContext.t check_function
+(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
+    [ctx1]. *)
 
 (** {6 Dumping to a file } *)
 
 val dump_universes :
-  (constraint_type -> string -> string -> unit) ->
-  universes -> unit
+  (constraint_type -> string -> string -> unit) -> t -> unit
+
+(** {6 Debugging} *)
+val check_universes_invariants : t -> unit
-- 
cgit v1.2.3