diff options
| author | Pierre-Marie Pédrot | 2018-09-27 17:00:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-09 14:10:27 +0100 |
| commit | 6e5dd2ee8bc014d1f99cef3156a5114b11510398 (patch) | |
| tree | dc3e41655419a8edd82d51029a0eb28e3b03d7ad /engine/univNames.ml | |
| parent | 27048fb3ef7a10ffde1ee368f6fb7ef354431fe8 (diff) | |
Remove remnants of polymorphic instance name registration.
Diffstat (limited to 'engine/univNames.ml')
| -rw-r--r-- | engine/univNames.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index 5c87fed31c..b7ccd2372f 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -53,8 +53,6 @@ let compute_instance_binders inst ubinders = in Array.map_to_list map (Instance.to_array inst) -let register_universe_binders ref ubinders = () - type univ_name_list = Names.lname list let universe_binders_with_opt_names ref names = |