diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-02 17:28:22 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-02 17:28:22 +0000 |
| commit | 556c2ce6f1b09d09484cc83f6ada213496add45b (patch) | |
| tree | fe48802a1c5876c42c9ed03dbb6d876030bf2aac /printing | |
| 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')
| -rw-r--r-- | printing/ppextra.ml | 20 | ||||
| -rw-r--r-- | printing/pptactic.ml | 4 |
2 files changed, 4 insertions, 20 deletions
diff --git a/printing/ppextra.ml b/printing/ppextra.ml deleted file mode 100644 index 8acdd2e1b..000000000 --- a/printing/ppextra.ml +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Genarg -open Ppextend -open Pptactic -open Extrawit - -let pr_tac_polymorphic n _ _ prtac = prtac (n,E) - -let _ = for i=0 to 5 do - let wit = wit_tactic i in - declare_extra_genarg_pprule wit - (pr_tac_polymorphic i) (pr_tac_polymorphic i) (pr_tac_polymorphic i) -done diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 3b3de2a3c..0fd3b454c 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) |