diff options
Diffstat (limited to 'library/universes.ml')
| -rw-r--r-- | library/universes.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/library/universes.ml b/library/universes.ml index b37970b38a..d8fa563a0e 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -144,8 +144,7 @@ let constr_of_global gr = else c let unsafe_constr_of_global gr = - let c, ctx = unsafe_global_instance (Global.env ()) gr in - c + unsafe_global_instance (Global.env ()) gr let constr_of_global_univ (gr,u) = match gr with |