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

---
 parsing/g_vernac.ml4 | 8 ++++----
 parsing/pcoq.ml      | 1 +
 parsing/pcoq.mli     | 1 +
 3 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4d6741ff5..941421853 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -10,10 +10,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
@@ -140,7 +140,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, ... *)
@@ -555,8 +555,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 fec26f941..7f18eb90e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -440,6 +440,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 1b330aa04..d94c30363 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -196,6 +196,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
-- 
cgit v1.2.3