From f84c0b96f11d5d1f130d36c0c04597ddeca6001f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 2 Sep 2017 18:19:34 +0200
Subject: Fix coq/ltac2#12: Error should name which match cases are unhandled.

---
 src/tac2intern.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'src/tac2intern.ml')

diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 88824386d9..b9e77f3cf5 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -953,12 +953,15 @@ and intern_case env loc e pl =
       intern_branch rem
     in
     let () = intern_branch pl in
-    let map = function
-    | None -> user_err ~loc (str "TODO: Unhandled match case") (** FIXME *)
+    let map n is_const = function
+    | None ->
+      let kn = match kn with Other kn -> kn | _ -> assert false in
+      let cstr = pr_internal_constructor kn n is_const in
+      user_err ~loc (str "Unhandled match case for constructor " ++ cstr)
     | Some x -> x
     in
-    let const = Array.map map const in
-    let nonconst = Array.map map nonconst in
+    let const = Array.mapi (fun i o -> map i true o) const in
+    let nonconst = Array.mapi (fun i o -> map i false o) nonconst in
     let ce = GTacCse (e', kn, const, nonconst) in
     (ce, ret)
   | PKind_open kn ->
-- 
cgit v1.2.3