diff options
| author | Hugo Herbelin | 2020-05-14 21:34:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-14 21:34:17 +0200 |
| commit | 56e23844e80e6d607ad5fa56dfeedcd70e97ee70 (patch) | |
| tree | 403c7b43e73fa4159fd997ca26953098b34e22b5 /interp/notation.mli | |
| parent | cc54af3842cbf99f169f7937b0e31f737652bd3a (diff) | |
| parent | b5ecd2e46202f47cfccf305e449bcdd8a6a14a0f (diff) | |
Merge PR #12256: Move the static check of evaluability in unfold tactic to runtime.
Reviewed-by: herbelin
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index b427aa9bb3..96a76c4de6 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -245,7 +245,8 @@ val availability_of_notation : specific_notation -> subscopes -> (** {6 Miscellaneous} *) -val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> +(** If head is true, also allows applied global references. *) +val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) -> notation_key -> delimiters option -> GlobRef.t (** Checks for already existing notations *) |