From cbba00588b9f35393460bc0c40dd6b04d9f4439a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 11 Feb 2020 16:07:24 +0100
Subject: Remove unused Environ.push_constraints_to_env

---
 kernel/environ.ml  |  3 ---
 kernel/environ.mli | 21 ++++++++++-----------
 2 files changed, 10 insertions(+), 14 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f04863386f..38bb56b92b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -399,9 +399,6 @@ let add_constraints c env =
 let check_constraints c env =
   UGraph.check_constraints c env.env_stratification.env_universes
 
-let push_constraints_to_env (_,univs) env =
-  add_constraints univs env
-
 let add_universes ~lbound ~strict ctx g =
   let g = Array.fold_left
             (fun g v -> UGraph.add_universe ~lbound ~strict v g)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index bd5a000c2b..2f76c12483 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -288,22 +288,21 @@ val lookup_modtype : ModPath.t -> env -> module_type_body
 
 (** {5 Universe constraints } *)
 
-(** Add universe constraints to the environment.
-    @raise UniverseInconsistency .
-*)
 val add_constraints : Univ.Constraint.t -> env -> env
+(** Add universe constraints to the environment.
+    @raise UniverseInconsistency. *)
 
-(** Check constraints are satifiable in the environment. *)
 val check_constraints : Univ.Constraint.t -> env -> bool
+(** Check constraints are satifiable in the environment. *)
+
 val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
-(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment.
-   @raise UGraph.AlreadyDeclared if one of the universes is already declared.
-*)
-val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
-(* [push_context_set ?(strict=false) ctx env] pushes the universe context set
-  to the environment. It does not fail if one of the universes is already declared. *)
+(** [push_context ?(strict=false) ctx env] pushes the universe context to the environment.
+    @raise UGraph.AlreadyDeclared if one of the universes is already declared. *)
 
-val push_constraints_to_env : 'a Univ.constrained -> env -> env
+val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
+(** [push_context_set ?(strict=false) ctx env] pushes the universe
+    context set to the environment. It does not fail even if one of the
+    universes is already declared. *)
 
 val push_subgraph : Univ.ContextSet.t -> env -> env
 (** [push_subgraph univs env] adds the universes and constraints in
-- 
cgit v1.2.3