From 8b2c4ea19c7930939c6d6d540558f042a60ac391 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Dec 2019 23:37:41 +0100 Subject: Making structure of type "tolerability" and related clearer. Also renamed it to relative_entry_level. Correspondence between old and new representation is: (n,L) -> LevelLt n (n,E), (n,Prec n) -> LevelLe n (n,Any) -> LevelSome (n,Prec p) when n<>p was unused Should not change global semantics (except error message in pr_arg). --- printing/printer.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'printing/printer.mli') diff --git a/printing/printer.mli b/printing/printer.mli index cd5151bd8f..24d0a8cf6a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -51,7 +51,7 @@ val enable_goal_names_printing : bool ref val pr_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t +val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" @@ -63,7 +63,7 @@ val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t val pr_econstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t -val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t +val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t @@ -100,7 +100,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t -val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t +val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t -- cgit v1.2.3