diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 472fddb829..fcd88fd543 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -329,7 +329,6 @@ let strengthen_const mp_from l cb resolver = let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_private_poly_univs = None; const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = |