diff options
| author | Arnaud Spiwack | 2015-07-23 09:46:21 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-09-25 10:40:10 +0200 |
| commit | d50aa51b4a3d39e708bc5ab3acb9f549857bceef (patch) | |
| tree | a4aa394b96d647a478779984e59c0515ce5ffff9 | |
| parent | e0547f9e9134a9fff122df900942a094c53535c3 (diff) | |
Add `Guarded` to the assumption tokens.
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
1 files changed, 7 insertions, 1 deletions
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 ] ] |