diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-09 16:08:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-09 16:08:48 +0200 |
| commit | 834530272b9006e28a4b7ba35b1f8f861f51e7ce (patch) | |
| tree | e485fd87323492daf135d7eecbb330a9e03fc0bb /interp/notation_ops.ml | |
| parent | f9ef634e94c667641a9da12fa2b9f8e585d6d5c6 (diff) | |
| parent | 8ad6bf357284f3fcfd94f08561450bb5bf38ad36 (diff) | |
Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while looking for a notation for a nested pattern
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index a0d69ce79..aa9a6ed0d 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1335,10 +1335,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = match DAst.get a1, a2 with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) - | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> + | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in sigma,(0,l) - | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) + | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in |