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/environ.ml | |
| parent | 4c6c173447d5b7d04aa0fd4f51d27a078c675708 (diff) | |
Remove unused Environ.push_constraints_to_env
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 3 |
1 files changed, 0 insertions, 3 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) |