From 26ed8658149d14efa6e4d077c573481281cb610e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 27 Aug 2016 06:48:46 +0200 Subject: Support qualified identifiers in Show Match (bug #5050). --- toplevel/vernacentries.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'toplevel/vernacentries.ml') diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dc098f1f0..33a8609a7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -120,9 +120,7 @@ let show_intro all = [Not_found] is raised if the given string isn't the qualid of a known inductive type. *) -let make_cases s = - let qualified_name = Libnames.qualid_of_string s in - let glob_ref = Nametab.locate qualified_name in +let make_cases_aux glob_ref = match glob_ref with | Globnames.IndRef i -> let {Declarations.mind_nparams = np} @@ -142,11 +140,16 @@ let make_cases s = carr tarr [] | _ -> raise Not_found +let make_cases s = + let qualified_name = Libnames.qualid_of_string s in + let glob_ref = Nametab.locate qualified_name in + make_cases_aux glob_ref + (** Textual display of a generic "match" template *) let show_match id = let patterns = - try make_cases (Id.to_string (snd id)) + try make_cases_aux (Nametab.global id) with Not_found -> error "Unknown inductive type." in let pr_branch l = -- cgit v1.2.3