From d50aa51b4a3d39e708bc5ab3acb9f549857bceef Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 23 Jul 2015 09:46:21 +0200
Subject: Add `Guarded` to the assumption tokens.

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

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b71028942b..263792ef0c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -73,11 +73,16 @@ let make_bullet s =
 
 type nl_assumption =
   | Positive
+  | Guarded
 let eq_nl_assumption x y =
   match x,y with
   | Positive,Positive -> true
+  | Guarded,Guarded -> true
+  | _ , _ -> false
 let check_positivity l =
   not (List.mem_f eq_nl_assumption Positive l)
+let check_guardedness l =
+  not (List.mem_f eq_nl_assumption Guarded l)
 
 let default_command_entry =
   Gram.Entry.of_parser "command_entry"
@@ -281,7 +286,8 @@ GEXTEND Gram
     [ [ IDENT "Assume"; "[" ; l=LIST1 nl_assumption ; "]" -> l | -> [] ] ]
   ;
   nl_assumption:
-    [ [ IDENT "Positive" -> Positive ] ]
+    [ [ IDENT "Positive" -> Positive
+      | IDENT "Guarded" -> Guarded ] ]
   ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
-- 
cgit v1.2.3