From 4c97e4ce19ca4c387039cfdcb4f24658100230b0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 1 Jul 2014 22:50:37 +0200
Subject: Add toplevel commands to declare global universes and constraints.

---
 intf/vernacexpr.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index af65f65414..5aa9d51fc3 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -303,6 +303,8 @@ type vernac_expr =
       locality option * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
+  | VernacUniverse of lident list
+  | VernacConstraint of (lident * Univ.constraint_type * lident) list
 
   (* Gallina extensions *)
   | VernacBeginSection of lident
-- 
cgit v1.2.3