From 6e884b01deaf2b9a7d012590c9e3f103d4091c4d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Apr 2020 18:21:37 +0200
Subject: Constrintern: As in terms, accept @C for C abbreviation in cases
 patterns.

---
 interp/constrintern.ml | 17 ++++++-----------
 1 file changed, 6 insertions(+), 11 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3