diff options
Diffstat (limited to 'interp/notation_ops.mli')
| -rw-r--r-- | interp/notation_ops.mli | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 280ccfd21f..576c5b943a 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -10,24 +10,28 @@ open Names open Notation_term open Glob_term -(** Utilities about [notation_constr] *) +(** {5 Utilities about [notation_constr]} *) -(** Translate a [glob_constr] into a notation given the list of variables - bound by the notation; also interpret recursive patterns *) +val eq_notation_constr : notation_constr -> notation_constr -> bool -val notation_constr_of_glob_constr : notation_interp_env -> - glob_constr -> notation_constr +(** Substitution of kernel names in interpretation data *) +val subst_interpretation : + Mod_subst.substitution -> interpretation -> interpretation + (** Name of the special identifier used to encode recursive notations *) + val ldots_var : Id.t -(** Equality of [glob_constr] (warning: only partially implemented) *) -(** FIXME: nothing to do here *) -val eq_glob_constr : glob_constr -> glob_constr -> bool +(** {5 Translation back and forth between [glob_constr] and [notation_constr] *) -val eq_notation_constr : notation_constr -> notation_constr -> bool +(** Translate a [glob_constr] into a notation given the list of variables + bound by the notation; also interpret recursive patterns *) + +val notation_constr_of_glob_constr : notation_interp_env -> + glob_constr -> notation_constr -(** Re-interpret a notation as a [glob_constr], taking care of binders *) +(** Re-interpret a notation as a [glob_constr], taking care of binders *) val glob_constr_of_notation_constr_with_binders : Loc.t -> ('a -> Name.t -> 'a * Name.t) -> @@ -36,6 +40,8 @@ val glob_constr_of_notation_constr_with_binders : Loc.t -> val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr +(** {5 Matching a notation pattern against a [glob_constr] *) + (** [match_notation_constr] matches a [glob_constr] against a notation interpretation; raise [No_match] if the matching fails *) @@ -55,9 +61,5 @@ val match_notation_constr_ind_pattern : ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (int * cases_pattern list) -(** Substitution of kernel names in interpretation data *) - -val subst_interpretation : - Mod_subst.substitution -> interpretation -> interpretation +(** {5 Matching a notation pattern against a [glob_constr] *) -val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list |