diff options
| author | Gaëtan Gilbert | 2020-02-11 16:07:24 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-11 16:07:24 +0100 |
| commit | cbba00588b9f35393460bc0c40dd6b04d9f4439a (patch) | |
| tree | 40509bf9804fe9d4ba3235f6001db7fa69a395b3 /kernel | |
| parent | 4c6c173447d5b7d04aa0fd4f51d27a078c675708 (diff) | |
Remove unused Environ.push_constraints_to_env
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 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 |