From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 checker/mod_checking.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index c33c6d5d09..b86d491d72 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -16,8 +16,8 @@ let check_constant_declaration env kn cb =
   (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
-    | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
-    | Polymorphic_const auctx ->
+    | Monomorphic ctx -> false, push_context_set ~strict:true ctx env
+    | Polymorphic auctx ->
       let ctx = Univ.AUContext.repr auctx in
       let env = push_context ~strict:false ctx env in
       true, env
-- 
cgit v1.2.3