From b49d803286ba9ed711313702bb4269c5e9c516fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 18 Dec 2014 16:35:46 +0100
Subject: Proof using: New vernacular to name sets of section variables

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

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index bc167d94a3..f66b1c1249 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -323,6 +323,7 @@ type vernac_expr =
       class_rawexpr * class_rawexpr
   | VernacIdentityCoercion of obsolete_locality * lident *
       class_rawexpr * class_rawexpr
+  | VernacNameSectionHypSet of lident * section_subset_descr 
 
   (* Type classes *)
   | VernacInstance of
-- 
cgit v1.2.3