diff options
| author | ppedrot | 2013-07-02 17:28:22 +0000 |
|---|---|---|
| committer | ppedrot | 2013-07-02 17:28:22 +0000 |
| commit | 556c2ce6f1b09d09484cc83f6ada213496add45b (patch) | |
| tree | fe48802a1c5876c42c9ed03dbb6d876030bf2aac /printing/pptactic.ml | |
| parent | 89abe2a141b3baa11bf0e8bcdecaf68220251c6e (diff) | |
Removing the use of leveled tactics wit_tacticn. It is now handled
through a unique generic argument, and the level is only considered
at parsing time.
This may introduce unnecessary parentheses in Ltac printing though,
as every tactic argument is collapsed at the lowest level. I assume
this does not matter that much, and anyway Ltac printing is quite
bugged as of today.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 3b3de2a3c7..0fd3b454ce 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1011,6 +1011,10 @@ let register_uniform_printer wit pr = let () = Genprint.register_print0 Constrarg.wit_intro_pattern pr_intro_pattern pr_intro_pattern pr_intro_pattern +let () = + let printer _ _ prtac = prtac (0, E) in + declare_extra_genarg_pprule wit_tactic printer printer printer + let _ = Hook.set Tactic_debug.tactic_printer (fun x -> pr_glob_tactic (Global.env()) x) |