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/environ.ml | |
| parent | 9700c44dca70f5550a6713e4ccbb3693e058a9a7 (diff) | |
| parent | cbba00588b9f35393460bc0c40dd6b04d9f4439a (diff) | |
Merge PR #11569: Remove unused Environ.push_constraints_to_env
Reviewed-by: ppedrot
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 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) |