diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-29 18:30:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-29 18:45:46 +0200 |
| commit | 8ad6bf357284f3fcfd94f08561450bb5bf38ad36 (patch) | |
| tree | 0875a95610c22592eaf52a15bb0d9dd502aad914 /interp/constrextern.ml | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Fixes #7110 ("as" untested while looking for notation for nested patterns).
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 19444988b..8f5ed98f1 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -479,7 +479,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function if is_inactive_rule keyrule then raise No_match; let loc = t.loc in match DAst.get t with - | PatCstr (cstr,_,na) -> + | PatCstr (cstr,args,na) -> + let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in let p = apply_notation_to_pattern ?loc (ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na |