Fix coq/ltac2#12: Error should name which match cases are unhandled.

3 files changed, 20 insertions, 8 deletions

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 ->
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 939f44aeaf..75ad2082d4 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -125,6 +125,15 @@ let find_constructor n empty def =
   in
   find n def
 
+let pr_internal_constructor tpe n is_const =
+  let data = match Tac2env.interp_type tpe with
+  | (_, GTydAlg data) -> data
+  | _ -> assert false
+  in
+  let id = find_constructor n is_const data.galg_constructors in
+  let kn = change_kn_label tpe id in
+  pr_constructor kn
+
 let order_branches cbr nbr def =
   let rec order cidx nidx def = match def with
   | [] -> []
@@ -179,18 +188,17 @@ let pr_glbexpr_gen lvl c =
     paren (prlist_with_sep (fun () -> str "," ++ spc ()) (pr_glbexpr E1) cl)
   | GTacCst (Other tpe, n, cl) ->
     begin match Tac2env.interp_type tpe with
-    | _, GTydAlg { galg_constructors = def } ->
+    | _, GTydAlg def ->
       let paren = match lvl with
       | E0 -> paren
       | E1 | E2 | E3 | E4 | E5 -> fun x -> x
       in
-      let id = find_constructor n (List.is_empty cl) def in
-      let kn = change_kn_label tpe id in
+      let cstr = pr_internal_constructor tpe n (List.is_empty cl) in
       let cl = match cl with
       | [] -> mt ()
       | _ -> spc () ++ pr_sequence (pr_glbexpr E0) cl
       in
-      paren (hov 2 (pr_constructor kn ++ cl))
+      paren (hov 2 (cstr ++ cl))
     | _, GTydRec def ->
       let args = List.combine def cl in
       let pr_arg ((id, _, _), arg) =
diff --git a/src/tac2print.mli b/src/tac2print.mli
index 0a04af2ff0..737e813ed3 100644
--- a/src/tac2print.mli
+++ b/src/tac2print.mli
@@ -24,6 +24,7 @@ val pr_glbtype : ('a -> string) -> 'a glb_typexpr -> Pp.t
 (** {5 Printing expressions} *)
 
 val pr_constructor : ltac_constructor -> Pp.t
+val pr_internal_constructor : type_constant -> int -> bool -> Pp.t
 val pr_projection : ltac_projection -> Pp.t
 val pr_glbexpr_gen : exp_level -> glb_tacexpr -> Pp.t
 val pr_glbexpr : glb_tacexpr -> Pp.t