From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- printing/printer.mli | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) (limited to 'printing/printer.mli') diff --git a/printing/printer.mli b/printing/printer.mli index 3424c41d..695ab33b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -10,7 +10,6 @@ open Pp open Names open Globnames open Term -open Context open Environ open Pattern open Evd @@ -109,13 +108,13 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds -val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds -val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds -val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds +val pr_var_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds +val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds +val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds -val pr_named_context : env -> evar_map -> named_context -> std_ppcmds +val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds val pr_named_context_of : env -> evar_map -> std_ppcmds -val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds +val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds val pr_rel_context_of : env -> evar_map -> std_ppcmds val pr_context_of : env -> evar_map -> std_ppcmds @@ -162,12 +161,16 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) (** Declarations for the "Print Assumption" command *) +type axiom = + | Constant of constant (* An axiom or a constant. *) + | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) + | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) + type context_object = - | Variable of Id.t (** A section variable or a Let definition *) - (** An axiom and the type it inhabits (if an axiom of the empty type) *) - | Axiom of constant * (Label.t * Context.rel_context * types) list - | Opaque of constant (** An opaque constant. *) - | Transparent of constant (** A transparent constant *) + | Variable of Id.t (* A section variable or a Let definition *) + | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Opaque of constant (* An opaque constant. *) + | Transparent of constant module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : CMap.ExtS -- cgit v1.2.3