diff options
| author | Hugo Herbelin | 2020-04-12 18:21:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-09 11:04:47 +0100 |
| commit | 6e884b01deaf2b9a7d012590c9e3f103d4091c4d (patch) | |
| tree | 66d3683dee66b77b99c4fb045225758008502a28 | |
| parent | ae2c4b508f6c03478d4915e4c309896fcfd92f82 (diff) | |
Constrintern: As in terms, accept @C for C abbreviation in cases patterns.
| -rw-r--r-- | interp/constrintern.ml | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 96af8f7fb2..d4090117b0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1759,17 +1759,12 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head)) end | CPatCstr (qid, Some expl_pl, pl) -> - let g = - try Nametab.locate qid - with Not_found as exn -> - let _, info = Exninfo.capture exn in - let info = Option.cata (Loc.add_loc info) info loc in - Exninfo.iraise (InternalizationError (NotAConstructor qid), info) - in - (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) - (* but not scopes in expl_pl *) - let (argscs1,_) = find_remaining_scopes expl_pl pl g in - DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat test_kind_inner scopes) pl, []) + begin + match drop_syndef test_kind scopes qid expl_pl with + | None -> Loc.raise ?loc (InternalizationError (NotAConstructor qid)) + | Some (g,syndef_pl,extra_expl_pl) -> + DAst.make ?loc @@ RCPatCstr (g, syndef_pl @ extra_expl_pl @ List.map (in_pat test_kind_inner scopes) pl, []) + end | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind test_kind_inner) (Number (SMinus,p)) scopes in |