From 556c2ce6f1b09d09484cc83f6ada213496add45b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 2 Jul 2013 17:28:22 +0000
Subject: 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
---
 dev/printers.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

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
-- 
cgit v1.2.3