diff options
| author | Pierre-Marie Pédrot | 2014-09-03 18:42:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-03 18:42:21 +0200 |
| commit | 6119a0e4f760ff944351570e90487f066db42858 (patch) | |
| tree | 7cf5adce852ca67186c014bd2d0d1beecf44c6bc | |
| parent | ce6fbc60662042873d02479f7f2fb40601058a2a (diff) | |
Fixing printing of unreachable local tactics.
| -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 87fb500ef0..890e0d585b 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 |