diff options
| author | Hugo Herbelin | 2020-02-23 17:09:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-23 18:05:32 +0100 |
| commit | 61f2f55a08dcef612c538ec7e6d0864d86fe3e0a (patch) | |
| tree | c7de9a5d4a363d266ca762c4fb9550c5f7811c2d /interp/notation_ops.ml | |
| parent | 5820b274acda8be0372471758842b0ea2b950d41 (diff) | |
Not iterating recursive notations more than once.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index d1eb50d370..9f052278ad 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -258,6 +258,8 @@ let glob_constr_of_notation_constr ?loc x = (******************************************************************************) (* Translating a glob_constr into a notation, interpreting recursive patterns *) +let print_parentheses = ref false + type found_variables = { vars : Id.t list; recursive_term_vars : (Id.t * Id.t) list; @@ -1092,6 +1094,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert = let rest = Id.List.assoc ldots_var terms in let t = Id.List.assoc y terms in let sigma = remove_sigma y (remove_sigma ldots_var sigma) in + if !print_parentheses && not (List.is_empty acc) then raise No_match; aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in |