From ed0c434a05a929a659e43aed80ab7c8179a7daa3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 13 Nov 2017 19:03:03 +0100
Subject: [api] Insert miscellaneous API deprecation back to core.

---
 vernac/command.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac/command.mli')

diff --git a/vernac/command.mli b/vernac/command.mli
index 5415d33080..fb99a717b9 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -127,24 +127,24 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+    recursive_preentry * Univdecls.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+    recursive_preentry * Univdecls.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   locality -> polymorphic ->
-  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+  recursive_preentry * Univdecls.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
-  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+  recursive_preentry * Univdecls.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
-- 
cgit v1.2.3