diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-03 18:42:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-03 18:42:21 +0200 |
| commit | 6119a0e4f760ff944351570e90487f066db42858 (patch) | |
| tree | 7cf5adce852ca67186c014bd2d0d1beecf44c6bc /printing/pptactic.ml | |
| parent | ce6fbc60662042873d02479f7f2fb40601058a2a (diff) | |
Fixing printing of unreachable local tactics.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 87fb500ef..890e0d585 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -343,7 +343,10 @@ let pr_ltac_or_var pr = function let pr_ltac_constant kn = if !Constrextern.in_debugger then pr_kn kn - else pr_qualid (Nametab.shortest_qualid_of_tactic kn) + else try + pr_qualid (Nametab.shortest_qualid_of_tactic kn) + with Not_found -> (* local tactic not accessible anymore *) + str "<" ++ pr_kn kn ++ str ">" let pr_evaluable_reference_env env = function | EvalVarRef id -> pr_id id |