diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 29 |
1 files changed, 21 insertions, 8 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 5cc4c835..fb22da83 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -341,7 +341,7 @@ let intern_typed_pattern ist p = let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = - try l, Inl (intern_evaluable ist r) + try Inl (intern_evaluable ist r) with e when Logic.catchable_exception e -> (* Compatibility. In practice, this means that the code above is useless. Still the idea of having either an evaluable @@ -356,19 +356,19 @@ let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let c = Constrintern.interp_reference sign r in match c with | GRef (_,r,None) -> - l, Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) + Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) | GVar (_,id) -> let r = evaluable_of_global_reference ist.genv (VarRef id) in - l, Inl (ArgArg (r,None)) + Inl (ArgArg (r,None)) | _ -> - l, Inr ((c,None),dummy_pat) in - match p with + Inr ((c,None),dummy_pat) in + (l, match p with | Inl r -> interp_ref r | Inr (CAppExpl(_,(None,r,None),[])) -> (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> - l, Inr (intern_typed_pattern ist c) + Inr (intern_typed_pattern ist c)) (* This seems fairly hacky, but it's the first way I've found to get proper globalization of [unfold]. --adamc *) @@ -809,11 +809,24 @@ let pr_ltac_fun_arg = function let print_ltac id = try let kn = Nametab.locate_tactic id in - let l,t = split_ltac_fun (Tacenv.interp_ltac kn) in + let entries = Tacenv.ltac_entries () in + let tac = KNmap.find kn entries in + let filter mp = + try Some (Nametab.shortest_qualid_of_module mp) + with Not_found -> None + in + let mods = List.map_filter filter tac.Tacenv.tac_redef in + let redefined = match mods with + | [] -> mt () + | mods -> + let redef = prlist_with_sep fnl pr_qualid mods in + fnl () ++ str "Redefined by:" ++ fnl () ++ redef + in + let l,t = split_ltac_fun tac.Tacenv.tac_body in hv 2 ( hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++ prlist pr_ltac_fun_arg l ++ spc () ++ str ":=") - ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) + ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined with Not_found -> errorlabstrm "print_ltac" |