diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ocamldebug-coq.template | 2 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/Makefile | 2 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 978623ad22..ac5ec1e0d5 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -19,7 +19,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ -I $COQTOP/translate \ -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \ - -I $COQTOP/contrib/fourier -I $COQTOP/contrib/first-order \ + -I $COQTOP/contrib/fourier -I $COQTOP/contrib/firstorder \ -I $COQTOP/contrib/interface -I $COQTOP/contrib/jprover \ -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile index 5a5b3b9752..7ab1bd3fcd 100644 --- a/dev/ocamlweb-doc/Makefile +++ b/dev/ocamlweb-doc/Makefile @@ -9,7 +9,7 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \ -I ../../contrib/xml -I ../../contrib/extraction \ -I ../../contrib/interface -I ../../contrib/fourier \ -I ../../contrib/jprover -I ../../contrib/cc \ - -I ../../contrib/funind -I ../../contrib/first-order \ + -I ../../contrib/funind -I ../../contrib/firstorder \ -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \ -I ../../contrib/recdef diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 97973df2b6..de68ce1e5c 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -748,7 +748,7 @@ Conflicts exists between integers and constrs. \nlsep \TERM{cc} %% contrib/field \nlsep \TERM{field}~\STAR{\tacconstr} -%% contrib/first-order +%% contrib/firstorder \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}} \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}} \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}} |