From 6b45f2d36929162cf92272bb60c2c245d9a0ead3 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 22 Jun 2012 15:14:30 +0000 Subject: Added an indirection with respect to Loc in Compat. As many [open Compat] were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/notation.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index 3f66f993a..d1446527f 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -54,7 +54,7 @@ val find_scope : scope_name -> scope (** Declare delimiters for printing *) val declare_delimiters : scope_name -> delimiters -> unit -val find_delimiters_scope : loc -> delimiters -> scope_name +val find_delimiters_scope : Loc.t -> delimiters -> scope_name (** {6 Declare and uses back and forth an interpretation of primitive token } *) @@ -68,7 +68,7 @@ type required_module = full_path * string list type cases_pattern_status = bool (** true = use prim token in patterns *) type 'a prim_token_interpreter = - loc -> 'a -> glob_constr + Loc.t -> 'a -> glob_constr type 'a prim_token_uninterpreter = glob_constr list * (glob_constr -> 'a option) * cases_pattern_status @@ -82,9 +82,9 @@ val declare_string_interpreter : scope_name -> required_module -> (** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) -val interp_prim_token : loc -> prim_token -> local_scopes -> +val interp_prim_token : Loc.t -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) -val interp_prim_token_cases_pattern_expr : loc -> (global_reference -> unit) -> prim_token -> +val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token -> local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; @@ -113,7 +113,7 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit (** Return the interpretation bound to a notation *) -val interp_notation : loc -> notation -> local_scopes -> +val interp_notation : Loc.t -> notation -> local_scopes -> interpretation * (notation_location * scope_name option) (** Return the possible notations for a given term *) @@ -137,7 +137,7 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *) (** {6 Miscellaneous} *) -val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> +val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) -> notation -> delimiters option -> global_reference (** Checks for already existing notations *) -- cgit v1.2.3