diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-20 01:23:26 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-20 01:23:26 +0200 |
| commit | 0c766b2e3b54d96713a79e40661653c5486822a8 (patch) | |
| tree | 2b1453b97049e2e29e98eb9799d64adc95045b8c | |
| parent | 40479227cba680496bf358e196e57a9a64f9c65b (diff) | |
Print Assumptions shows engagement.
Seems to be morally required since we have the -type-in-type flag.
| -rw-r--r-- | printing/printer.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 33b95c2f5..18e490225 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -742,7 +742,8 @@ module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) let pr_assumptionset env s = - if ContextObjectMap.is_empty s then + if ContextObjectMap.is_empty s && + engagement env = (PredicativeSet, StratifiedType) then str "Closed under the global context" else let safe_pr_constant env kn = @@ -788,6 +789,16 @@ let pr_assumptionset env s = let (vars, axioms, opaque, trans) = ContextObjectMap.fold fold s ([], [], [], []) in + let theory = + if is_impredicative_set env then + [str "Set is impredicative"] + else [] + in + let theory = + if type_in_type env then + str "Type hierarchy is collapsed (logic is inconsistent)" :: theory + else theory + in let opt_list title = function | [] -> None | l -> @@ -801,6 +812,7 @@ let pr_assumptionset env s = opt_list (str "Section Variables:") vars; opt_list (str "Axioms:") axioms; opt_list (str "Opaque constants:") opaque; + opt_list (str "Theory:") theory; ] in prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums) |