From a1f10626bed1db14ce116e9201ed05dadfc366b4 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 11 Sep 2018 14:32:22 +0200
Subject: Remove romega

---
 dev/ocamldebug-coq.run      | 2 +-
 dev/v8-syntax/syntax-v8.tex | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index bccd3fefb4..85bb04efe0 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -37,7 +37,7 @@ if [ -z "$GUESS_CHECKER" ]; then
         -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
         -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
         -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
-        -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
+        -I $COQTOP/plugins/ring \
 	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
         -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 6b7960c92f..dd3908c25f 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -765,8 +765,6 @@ Conflicts exists between integers and constrs.
 %% plugins/ring
 \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
 \nlsep \TERM{ring}~\STAR{\tacconstr}
-%% plugins/romega
-\nlsep \TERM{romega}
 \SEPDEF
 \DEFNT{orient}
        \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$}
-- 
cgit v1.2.3