diff options
| author | Arnaud Spiwack | 2016-06-07 09:52:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2016-06-14 20:01:37 +0200 |
| commit | d4f3a1a807d474050a4e91e16ff7813f1db7f537 (patch) | |
| tree | 68c91e818fd7d35789c514b3db06f77ed54b8968 /parsing | |
| parent | 64e94267cb80adc1b4df782cc83a579ee521b59b (diff) | |
Assume totality: dedicated type rather than bool
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ced2da7a52..3ad5e77fcf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -219,13 +219,13 @@ GEXTEND Gram 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"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (check_guardedness a,None, recs) + VernacFixpoint ({Declarations.check_guarded=check_guardedness a},None, recs) | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (check_guardedness a,Some Discharge, recs) + VernacFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, recs) | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (check_guardedness a,None, corecs) + VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},None, corecs) | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (check_guardedness a,Some Discharge, corecs) + VernacCoFixpoint ({Declarations.check_guarded=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) |