diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 40c7c7010..10bbdc358 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -122,9 +122,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} @@ -144,11 +142,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 = |