Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

1 files changed, 2 insertions, 2 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index 60056dfd90..2f516f4f3c 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,12 +107,12 @@ let transl_with_decl env base kind = function
     let c, ectx = interp_constr env sigma c in
     let poly = lookup_polymorphism env base kind fqid in
     begin match UState.check_univ_decl ~poly ectx udecl with
-      | Entries.Polymorphic_const_entry (nas, ctx) ->
+      | Entries.Polymorphic_entry (nas, ctx) ->
         let inst, ctx = Univ.abstract_universes nas ctx in
         let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
         let c = EConstr.to_constr sigma c in
         WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
-      | Entries.Monomorphic_const_entry ctx ->
+      | Entries.Monomorphic_entry ctx ->
         let c = EConstr.to_constr sigma c in
         WithDef (fqid,(c, None)), ctx
     end