diff options
| author | Matej Kosik | 2016-01-11 12:34:30 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-01-11 12:34:30 +0100 |
| commit | 78bad016e389cd78635d40281bfefd7136733b7e (patch) | |
| tree | 51f90da34d2444734868d7954412ac08ddc0f5c6 /printing/printer.mli | |
| parent | f8eb2ed4ddbe2199187696f51c42734014f4d9d0 (diff) | |
| parent | 9d991d36c07efbb6428e277573bd43f6d56788fc (diff) | |
merge
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 5c60b89366..bdb295a478 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 @@ -165,7 +164,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) 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 + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (** An opaque constant. *) | Transparent of constant (** A transparent constant *) |