From c46c64b0c89120404a939a5cc9b50acd0f315992 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 13 Nov 2009 13:50:32 +0000
Subject: Remove useless ppevd (which is identical to ppevm)

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

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index 6e25ef51e..251a969b9 100644
--- a/dev/include
+++ b/dev/include
@@ -30,7 +30,6 @@
 #install_printer  (* pftreestate *)  pppftreestate;;
 #install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
-#install_printer  (* evar_defs *)  ppevd;;
 #install_printer  (* clenv *) ppclenv;;
 #install_printer  (* env *) ppenv;;
 
-- 
cgit v1.2.3