diff options
| author | Hugo Herbelin | 2019-11-14 13:41:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:42 +0100 |
| commit | 9da7715108554a5105c012685e90b2fa563abf08 (patch) | |
| tree | d97038021444c19f43a7676044d9795c42cf2e69 /interp/notation_ops.mli | |
| parent | 8d80875d230bd8af5611ec04bced1e5a17d058b0 (diff) | |
In printing patterns, distinguish the case of a notation to @id.
This is a case which conventionally deactivates implicit arguments.
Diffstat (limited to 'interp/notation_ops.mli')
| -rw-r--r-- | interp/notation_ops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index c62dac013b..2ab8b620df 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -69,12 +69,12 @@ val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> val match_notation_constr_cases_pattern : 'a cases_pattern_g -> interpretation -> (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) * - (int * 'a cases_pattern_g list) + (bool * int * 'a cases_pattern_g list) val match_notation_constr_ind_pattern : inductive -> 'a cases_pattern_g list -> interpretation -> (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) * - (int * 'a cases_pattern_g list) + (bool * int * 'a cases_pattern_g list) (** {5 Matching a notation pattern against a [glob_constr]} *) |