diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ocamldebug-coq.run | 2 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 |
2 files changed, 1 insertions, 3 deletions
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$} |