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 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/printers.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 3a8a2cc3d8..c3d3ce7091 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -155,7 +155,6 @@ Pfedit Tactic_debug Decl_mode Ppconstr -Extrawit Pcoq Printer Pptactic |