From 8f64e84a3560bcf668b00ac93ab33542456a9bda Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 23 Jul 2015 09:51:18 +0200 Subject: 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. --- parsing/g_vernac.ml4 | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 263792ef0c..ced2da7a52 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) -- cgit v1.2.3