diff options
| author | Gaëtan Gilbert | 2017-09-21 11:14:11 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-25 14:18:35 +0100 |
| commit | d071eac98b7812ac5c03004b438022900885d874 (patch) | |
| tree | f0f72dba7daf7c91ea2eda0332b568c4615ad3c9 /engine/evd.ml | |
| parent | 765392492df2f5e065b2b5e706b6620846337cc0 (diff) | |
Forbid repeated names in universe binders.
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 9ea2cc00f5..0f17e0dc6d 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -935,9 +935,6 @@ let nf_constraints evd = let universe_of_name evd s = UState.universe_of_name evd.universes s -let add_universe_name evd s l = - { evd with universes = UState.add_universe_name evd.universes s l } - let universe_binders evd = UState.universe_binders evd.universes let universes evd = UState.ugraph evd.universes |