diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:27:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:46:52 +0100 |
| commit | 03e21974a3e971a294533bffb81877dc1bd270b6 (patch) | |
| tree | 1b37339378f6bc93288b61f707efb6b08f992dc5 /printing | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 1 | ||||
| -rw-r--r-- | printing/printer.mli | 12 | ||||
| -rw-r--r-- | printing/printmod.ml | 4 |
3 files changed, 9 insertions, 8 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index e4bb89304..751e91cf0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -11,6 +11,7 @@ open CErrors open Util open Names open Term +open Constr open Environ open Globnames open Nametab diff --git a/printing/printer.mli b/printing/printer.mli index e74f47efe..cd6e6d63a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -8,7 +8,7 @@ open Names open Globnames -open Term +open Constr open Environ open Pattern open Evd @@ -95,15 +95,15 @@ val pr_constr_pattern : constr_pattern -> Pp.t val pr_cases_pattern : cases_pattern -> Pp.t -val pr_sort : evar_map -> sorts -> Pp.t +val pr_sort : evar_map -> Sorts.t -> Pp.t (** Universe constraints *) val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t -val pr_universe_instance : evar_map -> Univ.universe_context -> Pp.t -val pr_universe_ctx : evar_map -> Univ.universe_context -> Pp.t -val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> Pp.t +val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t +val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) @@ -198,7 +198,7 @@ module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet val pr_assumptionset : - env -> Term.types ContextObjectMap.t -> Pp.t + env -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : Id.t -> Pp.t diff --git a/printing/printmod.ml b/printing/printmod.ml index d4b756346..6b3b177aa 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -7,7 +7,7 @@ (************************************************************************) open Util -open Term +open Constr open Pp open Names open Environ @@ -149,7 +149,7 @@ let print_mutual_inductive env mind mib = let get_fields = let rec prodec_rec l subst c = - match kind_of_term c with + match kind c with | Prod (na,t,c) -> let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c |