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 | |
| parent | 5820b274acda8be0372471758842b0ea2b950d41 (diff) | |
Not iterating recursive notations more than once.
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 3 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 2 |
3 files changed, 6 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bdfb63add3..3a0c6648cf 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -59,7 +59,7 @@ let print_coercions = ref false (* This forces printing of parentheses even when it is implied by associativity/precedence *) -let print_parentheses = ref false +let print_parentheses = Notation_ops.print_parentheses (* This forces printing universe names of Type{.} *) let print_universes = Detyping.print_universes 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 diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index c62dac013b..d235f87580 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -61,6 +61,8 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const exception No_match +val print_parentheses : bool ref + val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list * ('a cases_pattern_disjunction_g * extended_subscopes) list * |