diff options
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 58 |
1 files changed, 37 insertions, 21 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f617faa3..8ab70283 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Term open Termops +open EConstr open Environ open Libnames open Globnames @@ -18,13 +20,14 @@ open Constrexpr open Notation_term open Notation open Misctypes +open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) -val extern_cases_pattern : Id.Set.t -> cases_pattern -> cases_pattern_expr -val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr -val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr +val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr +val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr @@ -37,11 +40,11 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr -val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference +val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr -val extern_sort : Evd.evar_map -> sorts -> glob_sort +val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> - Context.Rel.t -> local_binder list + rel_context -> local_binder_expr list (** Printing options *) val print_implicits : bool ref @@ -55,19 +58,22 @@ val print_projections : bool ref (** Customization of the global_reference printer *) val set_extern_reference : - (Loc.t -> Id.Set.t -> global_reference -> reference) -> unit + (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit val get_extern_reference : - unit -> (Loc.t -> Id.Set.t -> global_reference -> reference) + unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -(** This governs printing of implicit arguments. If [with_implicits] is - on and not [with_arguments] then implicit args are printed prefixed - by "!"; if [with_implicits] and [with_arguments] are both on the - function and not the arguments is prefixed by "!" *) -val with_implicits : ('a -> 'b) -> 'a -> 'b -val with_arguments : ('a -> 'b) -> 'a -> 'b +(** WARNING: The following functions are evil due to + side-effects. Think of the following case as used in the printer: -(** This forces printing of coercions *) -val with_coercions : ('a -> 'b) -> 'a -> 'b + without_specific_symbols [SynDefRule kn] (pr_glob_constr_env env) c + + vs + + without_specific_symbols [SynDefRule kn] pr_glob_constr_env env c + + which one is wrong? We should turn this kind of state into an + explicit argument. +*) (** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b @@ -80,3 +86,13 @@ val without_specific_symbols : interp_rule list -> ('a -> 'b) -> 'a -> 'b (** This prints metas as anonymous holes *) val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b + +(** Fine-grained activation and deactivation of notation printing. + *) +val toggle_scope_printing : + scope:Notation_term.scope_name -> activate:bool -> unit + +val toggle_notation_printing : + ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit + + |