Merge PR #6790: Allow universe declarations for [with Definition].

16 files changed, 62 insertions, 32 deletions

diff --git a/CHANGES b/CHANGES
index 466b4cde5..ab6aab0ee 100644
--- a/CHANGES
+++ b/CHANGES
@@ -86,6 +86,8 @@ Universes
   more information.
 - Fix #5726: Notations that start with `Type` now support universe instances
   with `@{u}`.
+- `with Definition` now understands universe declarations
+  (like `@{u| Set < u}`).
 
 Checker
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 92264fb72..887685585 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -62,18 +62,19 @@ let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
 let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
       WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
-  | CWith_Definition ((_,fqid),c) ->
-    let sigma = Evd.from_env env in
+  | CWith_Definition ((_,fqid),udecl,c) ->
+    let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
     let c, ectx = interp_constr env sigma c in
-    if Flags.is_universe_polymorphism () then
-      let ctx = UState.context ectx in
-      let inst, ctx = Univ.abstract_universes ctx in
-      let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
-      let c = EConstr.to_constr sigma c in
-      WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
-    else
-      let c = EConstr.to_constr sigma c in
-      WithDef (fqid,(c, None)), UState.context_set ectx
+    begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
+      | Entries.Polymorphic_const_entry ctx ->
+        let inst, ctx = Univ.abstract_universes ctx in
+        let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
+        let c = EConstr.to_constr sigma c in
+        WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
+      | Entries.Monomorphic_const_entry ctx ->
+        let c = EConstr.to_constr sigma c in
+        WithDef (fqid,(c, None)), ctx
+    end
 
 let loc_of_module l = l.CAst.loc
 
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 474b80ec4..b0a769c5a 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -17,6 +17,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 =
@@ -139,7 +144,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 7e9bc8caa..0a6e5b3b3 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -160,11 +160,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 =
@@ -536,3 +531,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"]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 595a60f33..feaef3161 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -12,10 +12,10 @@ open Pp
 open CErrors
 open Util
 open Names
+open Vernacexpr
 open Constrexpr
 open Constrexpr_ops
 open Extend
-open Vernacexpr
 open Decl_kinds
 open Declarations
 open Misctypes
@@ -142,7 +142,7 @@ let name_of_ident_decl : ident_decl -> name_decl =
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    record_field decl_notation rec_definition ident_decl;
+    record_field decl_notation rec_definition ident_decl univ_decl;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -557,8 +557,8 @@ GEXTEND Gram
     [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
   ;
   with_declaration:
-    [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
-          CWith_Definition (fqid,c)
+    [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
+          CWith_Definition (fqid,udecl,c)
       | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
 	  CWith_Module (fqid,qid)
       ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9aae251f1..258c4bb11 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -442,6 +442,7 @@ module Prim =
 
     let name = Gram.entry_create "Prim.name"
     let identref = Gram.entry_create "Prim.identref"
+    let univ_decl = Gram.entry_create "Prim.univ_decl"
     let ident_decl = Gram.entry_create "Prim.ident_decl"
     let pattern_ident = Gram.entry_create "pattern_ident"
     let pattern_identref = Gram.entry_create "pattern_identref"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8592968dc..e66aa4ade 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -198,6 +198,7 @@ module Prim :
     val ident : Id.t Gram.entry
     val name : lname Gram.entry
     val identref : lident Gram.entry
+    val univ_decl : universe_decl_expr Gram.entry
     val ident_decl : ident_decl Gram.entry
     val pattern_ident : Id.t Gram.entry
     val pattern_identref : lident Gram.entry
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
index 242eb802f..305d045b1 100644
--- a/pretyping/univdecls.mli
+++ b/pretyping/univdecls.mli
@@ -14,8 +14,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
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 8551d040d..2b7d643d6 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -233,9 +233,9 @@ open Decl_kinds
     hov 2 (keyword "Hint "++ pph ++ opth)
 
   let pr_with_declaration pr_c = function
-    | CWith_Definition (id,c) ->
+    | CWith_Definition (id,udecl,c) ->
       let p = pr_c c in
-      keyword "Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p
+      keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
     | CWith_Module (id,qid) ->
       keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
         pr_located pr_qualid qid
diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v
new file mode 100644
index 000000000..e68345516
--- /dev/null
+++ b/test-suite/modules/WithDefUBinders.v
@@ -0,0 +1,15 @@
+
+Set Universe Polymorphism.
+Module Type T.
+  Axiom foo@{u v|u < v} : Type@{v}.
+End T.
+
+Module M : T with Definition foo@{u v} := Type@{u} : Type@{v}.
+  Definition foo@{u v} := Type@{u} : Type@{v}.
+End M.
+
+Fail Module M' : T with Definition foo := Type.
+
+(* Without the binder expression we have to do trickery to get the
+   universes in the right order. *)
+Module M' : T with Definition foo := let t := Type in t.
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index f235de350..56e324376 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 (** {6 Parameters/Assumptions} *)
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
-  Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool
+  Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 0d6367291..6f81c4575 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -17,7 +17,7 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition : program_mode:bool ->
-  Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
+  Id.t -> definition_kind -> universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
 
@@ -27,6 +27,6 @@ val do_definition : program_mode:bool ->
 
 (** Not used anywhere. *)
 val interp_definition :
-  Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
+  universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
                         Univdecls.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index edfe7aa81..a794c2db0 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -14,7 +14,6 @@ open Pretyping
 open Evarutil
 open Evarconv
 open Misctypes
-open Vernacexpr
 
 module RelDecl = Context.Rel.Declaration
 
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index b181984e0..36c2993af 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -32,7 +32,7 @@ val do_cofixpoint :
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
-  fix_univs : Vernacexpr.universe_decl_expr option;
+  fix_univs : Constrexpr.universe_decl_expr option;
   fix_annot : Misctypes.lident option;
   fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 457a1da05..c59286d1a 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -57,7 +57,7 @@ let push_types env idl tl =
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : Vernacexpr.universe_decl_expr option;
+  ind_univs : universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index b8d85c8d9..833935724 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -47,7 +47,7 @@ val declare_mutual_inductive_with_eliminations :
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : Vernacexpr.universe_decl_expr option;
+  ind_univs : universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }