diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 15:11:01 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 15:11:01 +0200 |
| commit | 8886dfd8fbb53d8305f2aa72afab8377b3fa75b7 (patch) | |
| tree | 298827ee49b092dd23e7b584904c6d2e74666ef9 /printing/printer.ml | |
| parent | caf8402e4af75d85223e10cba68a6a145e050dab (diff) | |
Show assumptions of well-foundedness in `Print Assumptions`
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index b57fa9079..8609b19c9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -735,6 +735,8 @@ let pr_assumptionset env s = safe_pr_constant env kn ++ safe_pr_ltype typ | Positive m -> hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + | Guarded kn -> + hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") in let fold t typ accu = let (v, a, o, tr) = accu in |