From 902032b9293afacd6c3e16e5e161dd678664bd58 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 15 Jun 2015 10:17:27 +0200
Subject: Granting, undocumentedly, parsing of "Conjectures" as a synonym of
 "Conjecture" (see #4252).

---
 parsing/g_vernac.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 09059b410..e8a1b512c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -249,7 +249,8 @@ GEXTEND Gram
     [ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
       | IDENT "Variables" -> (Some Discharge, Definitional)
       | IDENT "Axioms" -> (None, Logical)
-      | IDENT "Parameters" -> (None, Definitional) ] ]
+      | IDENT "Parameters" -> (None, Definitional)
+      | IDENT "Conjectures" -> (None, Conjectural) ] ]
   ;
   inline:
     [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
-- 
cgit v1.2.3