diff options
| author | Pierre-Marie Pédrot | 2020-02-12 15:32:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-12 15:32:04 +0100 |
| commit | 99a0e8f01fd2570672e5e9d133d5a9472eef406b (patch) | |
| tree | 0e56954ff9a0775fcd1354b139ec1fe3eb56d47e /kernel | |
| parent | 9700c44dca70f5550a6713e4ccbb3693e058a9a7 (diff) | |
| parent | cbba00588b9f35393460bc0c40dd6b04d9f4439a (diff) | |
Merge PR #11569: Remove unused Environ.push_constraints_to_env
Reviewed-by: ppedrot
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 3 | ||||
| -rw-r--r-- | kernel/environ.mli | 21 |
2 files changed, 10 insertions, 14 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 87f2f234da..501ac99ff3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -398,9 +398,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 e80d0a9b9f..a596584cbe 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -286,22 +286,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 |