diff options
| author | Maxime Dénès | 2017-06-19 17:43:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-19 17:43:19 +0200 |
| commit | 414890675cb72fd9286e19521a746677c06e784e (patch) | |
| tree | 14599a23215356ac472ac483ad564c11eb53c1fc /dev | |
| parent | 396c77feb0cced3965f90f65c681e48c528636d5 (diff) | |
| parent | 15b1856edd593b39d63d23584a4f5acec0eeb592 (diff) | |
Merge PR#613: Cumulativity for inductive types
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/include | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 1 |
4 files changed, 3 insertions, 4 deletions
diff --git a/dev/base_include b/dev/base_include index f9af0696b1..8ee1cceb23 100644 --- a/dev/base_include +++ b/dev/base_include @@ -58,8 +58,6 @@ (* Open main files *) -open API -open Grammar_API open Names open Term open Vars diff --git a/dev/include b/dev/include index 0f43f00729..31ae5da71a 100644 --- a/dev/include +++ b/dev/include @@ -41,6 +41,8 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; +#install_printer (* cumulativity info *) ppcumulativity_info;; +#install_printer (* abstract cumulativity info *) ppabstract_cumulativity_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6ae5125f6d..ff575e432c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -8,7 +8,6 @@ (* Printers for the ocaml toplevel. *) -open API open Util open Pp open Names @@ -215,6 +214,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx +let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index be6b914b6b..afa94a63e0 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,4 +1,3 @@ -open API open Format open Term open Names |