diff options
| author | Théo Zimmermann | 2018-09-26 13:12:46 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-26 13:12:46 +0200 |
| commit | 8292c485bde7911bf8a4d626faf9292ba0016e97 (patch) | |
| tree | 7c405894abe205031c0b0d9c4410a13a1efe38a6 /dev | |
| parent | b7cd70b5732d43280fc646115cd8597f2e844f95 (diff) | |
| parent | a1f10626bed1db14ce116e9201ed05dadfc366b4 (diff) | |
Merge PR #8419: Remove romega in favor of lia
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$} |