diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 14:03:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:32 +0200 |
| commit | 012fe1a96ba81ab0a7fa210610e3f25187baaf1d (patch) | |
| tree | 32282ac2f1198738c8c545b19215ff0a0d9ef6ce /printing/prettyp.mli | |
| parent | b720cd3cbefa46da784b68a8e016a853f577800c (diff) | |
Referring to evars by names. Added a parser for evars (but parsing of
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
Diffstat (limited to 'printing/prettyp.mli')
| -rw-r--r-- | printing/prettyp.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 595637745..9d558733a 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -27,8 +27,8 @@ val print_full_context_typ : unit -> std_ppcmds val print_full_pure_context : unit -> std_ppcmds val print_sec_context : reference -> std_ppcmds val print_sec_context_typ : reference -> std_ppcmds -val print_judgment : env -> unsafe_judgment -> std_ppcmds -val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds +val print_judgment : env -> Evd.evar_map -> unsafe_judgment -> std_ppcmds +val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds @@ -69,7 +69,7 @@ type object_pr = { print_named_decl : Id.t * constr option * types -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds } |