diff options
| -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 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) |