From 36e41e7581c86214a9f0f97436eb96a75b640834 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 9 Nov 2013 07:08:59 +0000
Subject: Revert the previous commit. It broke Coq compilation.

Tactics notation interpretation was messed up because of the use of
identical keys for different notations. All my tentative fixes were
unsuccessful, so better blankly revert the commit for now.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics/tactics.mllib')

diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index f1227c234..7b91665ad 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -15,7 +15,6 @@ Equality
 Contradiction
 Inv
 Leminv
-Tacenv
 Tacsubst
 Taccoerce
 Tacintern
-- 
cgit v1.2.3