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 /printing | |
| parent | 4a73e6b2bfb75451bcda7c74cf7478726a459799 (diff) | |
Add corresponding field in `VernacInductive`.
Makes sure not to generate inductive schemes of assumed positive types.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 832c08fe0e..a65bfd44d7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -761,7 +761,7 @@ module Make (pr_assumption_token (n > 1) stre ++ spc() ++ pr_ne_params_list pr_lconstr_expr l) ) - | VernacInductive (p,f,l) -> + | VernacInductive (chk,p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ |