diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
| commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
| tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /printing/printer.mli | |
| parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) | |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 25 |
1 files changed, 14 insertions, 11 deletions
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 |