From e5b94c29ff49f8b880290a72519157d26351bc6c Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 24 Dec 2010 23:49:15 +0000
Subject: Remove obsolete script univdot, update dev doc about universes

By the way, definitely remove "Dump Universes", which has been
deprecated since 2006 (r9306).

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

(limited to 'dev/v8-syntax')

diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 4fb47bea7b..6630be06ab 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -977,7 +977,6 @@ $$
 \nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{ident}
 \nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{string}
 \nlsep \TERM{Declare}~\TERM{ML}~\TERM{Module}~\PLUS{\NT{string}}
-\nlsep \TERM{Dump}~\TERM{Universes}~\OPT{\NT{string}}
 \nlsep \TERM{Locate}~\NT{locatable}
 \nlsep \TERM{Add}~\OPT{\TERM{Rec}}~\TERM{LoadPath}~\NT{string}~\OPT{\NT{as-dirpath}}
 \nlsep \TERM{Remove}~\TERM{LoadPath}~\NT{string}
-- 
cgit v1.2.3