diff options
| author | coqbot-app[bot] | 2020-10-12 12:53:02 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-12 12:53:02 +0000 |
| commit | a78b394d372f259107017cdb129be3fe53a15894 (patch) | |
| tree | eef0043d55f2ec739b48906f4b16b9b61d162e41 /interp/constrextern.ml | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
| parent | 3e32cf5b791cb5653520f68cd3d2677733b32324 (diff) | |
Merge PR #12950: Notations: reworking the treatment of only-parsing and only-printing notations
Reviewed-by: SkySkimmer
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 43fef8685d..167ea3ecdf 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -551,7 +551,7 @@ and extern_notation_pattern allscopes vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; let loc = t.loc in match DAst.get t with | PatCstr (cstr,args,na) -> @@ -568,7 +568,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; apply_notation_to_pattern (GlobRef.IndRef ind) (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with @@ -1238,7 +1238,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; let f,args = match DAst.get t with | GApp (f,args) -> f,args |