diff options
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 93322b760..fbba14ede 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 |