From f597952e1b216ca5adf9f782c736f4cfe705ef02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Jun 2019 19:09:25 +0200
Subject: Duplicate the type of constant entries in Proof_global.

This allows to desynchronize the kernel-facing API from the proof-facing one.
---
 engine/uState.ml  | 4 ++--
 engine/uState.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index 6a1282203a..bd61112f08 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -452,9 +452,9 @@ let restrict ctx vars =
   let uctx' = restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
-let demote_seff_univs entry uctx =
+let demote_seff_univs universes uctx =
   let open Entries in
-  match entry.const_entry_universes with
+  match universes with
   | Polymorphic_entry _ -> uctx
   | Monomorphic_entry (univs, _) ->
     let seff = LSet.union uctx.uctx_seff_univs univs in
diff --git a/engine/uState.mli b/engine/uState.mli
index 204e97eb15..9689f2e961 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -100,7 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
    universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
-val demote_seff_univs : 'a Entries.definition_entry -> t -> t
+val demote_seff_univs : Entries.universes_entry -> t -> t
 
 type rigid = 
   | UnivRigid
-- 
cgit v1.2.3