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 /interp | |
| parent | 27048fb3ef7a10ffde1ee368f6fb7ef354431fe8 (diff) | |
Remove remnants of polymorphic instance name registration.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 29e777d0c6..fe8fc7c969 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -520,7 +520,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - UnivNames.register_universe_binders gr pl + () else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c |