diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-07-23 09:51:18 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 10:40:10 +0200 |
| commit | 8f64e84a3560bcf668b00ac93ab33542456a9bda (patch) | |
| tree | add4c41cf4e25d902b894e94cb19a8d3c0a7d496 | |
| parent | d50aa51b4a3d39e708bc5ab3acb9f549857bceef (diff) | |
Add (temporary) syntax for assuming guardedness in (co-)fixed points.
The syntax is `Fixpoint Assume[Guarded] …`. For some reason `Assume [Guarded] Fixpoint` broke the parser.
| -rw-r--r-- | parsing/g_vernac.ml4 | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 263792ef0..ced2da7a5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -218,14 +218,14 @@ GEXTEND Gram let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (check_positivity a,priv,f,indl) - | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (true,None, recs) - | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (true,Some Discharge, recs) - | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (true,None, corecs) - | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (true,Some Discharge, corecs) + | "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (check_guardedness a,None, recs) + | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (check_guardedness a,Some Discharge, recs) + | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (check_guardedness a,None, corecs) + | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (check_guardedness a,Some Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) |