diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/library/global.ml b/library/global.ml index cb6334c74..3a74f535d 100644 --- a/library/global.ml +++ b/library/global.ml @@ -126,9 +126,8 @@ let opaque_tables () = Environ.opaque_tables (env ()) let instantiate cb c = let open Declarations in match cb.const_universes with - | Monomorphic_const _ -> c - | Polymorphic_const ctx -> - Vars.subst_instance_constr (Univ.AUContext.instance ctx) c + | Monomorphic_const _ -> c, Univ.AUContext.empty + | Polymorphic_const ctx -> c, ctx let body_of_constant_body cb = let open Declarations in |