diff options
| author | Arnaud Spiwack | 2015-06-23 17:45:04 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-06-24 17:55:47 +0200 |
| commit | 2adff76c5466734c633923e768c9dcbdc6f28c86 (patch) | |
| tree | aca997d04a076e09ce62929415cd66820a5c92d3 /parsing | |
| parent | 4a73e6b2bfb75451bcda7c74cf7478726a459799 (diff) | |
Add corresponding field in `VernacInductive`.
Makes sure not to generate inductive schemes of assumed positive types.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e8a1b512c0..be11b86adb 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -204,7 +204,7 @@ GEXTEND Gram indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (priv,f,indl) + VernacInductive (true,priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> |