diff options
| author | Guillaume Melquiond | 2016-08-27 06:48:46 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-08-27 06:48:46 +0200 |
| commit | 26ed8658149d14efa6e4d077c573481281cb610e (patch) | |
| tree | 573900ad783ec67dd4a2207b9ac8b30054df7ab3 | |
| parent | 7244637f251272c0d0155d49fc7c1af255b7cef8 (diff) | |
Support qualified identifiers in Show Match (bug #5050).
| -rw-r--r-- | intf/vernacexpr.mli | 2 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
4 files changed, 10 insertions, 7 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 156e00368d..ed44704df4 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -106,7 +106,7 @@ type showable = | ShowTree | ShowProofNames | ShowIntros of bool - | ShowMatch of lident + | ShowMatch of reference | ShowThesis type comment = diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index b0ff8b64f2..1e3c4b880b 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -88,7 +88,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) - | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) + | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 0d47b34dfd..40ce28dc0c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -591,7 +591,7 @@ module Make | ShowTree -> keyword "Show Tree" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") - | ShowMatch id -> keyword "Show Match " ++ pr_lident id + | ShowMatch id -> keyword "Show Match " ++ pr_reference id | ShowThesis -> keyword "Show Thesis" in return (pr_showable s) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dc098f1f00..33a8609a77 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 = |