From 88f3b5a441a3aaeb637d0b109544fbe71b7560dd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 20 Feb 2018 15:35:25 +0100
Subject: Allow universe declarations for [with Definition].

---
 pretyping/univdecls.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
index 706d3a157f..0bae49d434 100644
--- a/pretyping/univdecls.mli
+++ b/pretyping/univdecls.mli
@@ -12,8 +12,8 @@ type universe_decl =
 
 val default_univ_decl : universe_decl
 
-val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr ->
+val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr ->
                        Evd.evar_map * universe_decl
 
-val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option ->
+val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option ->
                        Evd.evar_map * universe_decl
-- 
cgit v1.2.3