diff options
| -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 |