From 74826c1869a423b4e7224d3f69180584bdef1726 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 27 Sep 2017 16:54:41 +0200
Subject: Parse [Proof using Type] without translating Type to an id.

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

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 4a471d4a2b..bc7146884c 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -236,6 +236,7 @@ type scheme =
 
 type section_subset_expr =
   | SsEmpty
+  | SsType
   | SsSingl of lident
   | SsCompl of section_subset_expr
   | SsUnion of section_subset_expr * section_subset_expr
-- 
cgit v1.2.3