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].

---
 intf/constrexpr.ml |  7 ++++++-
 intf/vernacexpr.ml | 16 +++++++++++-----
 2 files changed, 17 insertions(+), 6 deletions(-)

(limited to 'intf')

diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 5b51953bbe..695c8fcb91 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -15,6 +15,11 @@ open Decl_kinds
 
 (** [constr_expr] is the abstract syntax tree produced by the parser *)
 
+type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
+
+type ident_decl = lident * universe_decl_expr option
+type name_decl = lname * universe_decl_expr option
+
 type notation = string
 
 type explicitation =
@@ -137,7 +142,7 @@ type constr_pattern_expr = constr_expr
 
 type with_declaration_ast =
   | CWith_Module of Id.t list Loc.located * qualid Loc.located
-  | CWith_Definition of Id.t list Loc.located * constr_expr
+  | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr
 
 type module_ast_r =
   | CMident of qualid
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index ba28eaceaa..d81f4f0ba8 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -158,11 +158,6 @@ type option_ref_value =
 
 (** Identifier and optional list of bound universes and constraints. *)
 
-type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
-
-type ident_decl = lident * universe_decl_expr option
-type name_decl = lname * universe_decl_expr option
-
 type sort_expr = Sorts.family
 
 type definition_expr =
@@ -534,3 +529,14 @@ type vernac_when =
   | VtNow
   | VtLater
 type vernac_classification = vernac_type * vernac_when
+
+
+(** Deprecated stuff *)
+type universe_decl_expr = Constrexpr.universe_decl_expr
+[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"]
+
+type ident_decl = Constrexpr.ident_decl
+[@@ocaml.deprecated "alias of Constrexpr.ident_decl"]
+
+type name_decl = Constrexpr.name_decl
+[@@ocaml.deprecated "alias of Constrexpr.name_decl"]
-- 
cgit v1.2.3