diff options
| author | Amin Timany | 2017-06-01 16:18:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:51:19 +0200 |
| commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
| tree | ebab76cc4dedaf307f96088a3756d8292a341433 /dev | |
| parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) | |
Clean up universes of constants and inductives
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 |
3 files changed, 3 insertions, 3 deletions
diff --git a/dev/base_include b/dev/base_include index f9af0696b1..98cf67256f 100644 --- a/dev/base_include +++ b/dev/base_include @@ -196,7 +196,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; +(*let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;*) let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/dev/include b/dev/include index 4835b360db..1d87456de7 100644 --- a/dev/include +++ b/dev/include @@ -41,7 +41,7 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* univ info *) ppuniverse_info;; +#install_printer (* univ info *) ppcumulativity_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 e902da0b19..abf6db1b7f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -215,7 +215,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverse_info c = pp (Univ.pr_universe_info_ind Univ.Level.pr c) +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)) |