Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

Commit ce9c93c2 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Ensure compatibility with Coq 8.14 (fix #6).

parent e5047abc
Pipeline #260142 passed with stages
in 25 minutes and 54 seconds
......@@ -68,7 +68,7 @@ src/Tactic_float.v: src/Tactic_bignum.v src/Tactic_primfloat.v Remakefile
@COQC@ @COQEXTRAFLAGS@ -R src Interval $<
COQPKGS = clib engine kernel interp lib library parsing pretyping printing proofs tactics toplevel vernac plugins.ltac
PACKAGES = $(addprefix -package coq., $(COQPKGS)) -package @BIGINTPKG@
PACKAGES = $(addprefix -package @COQROOT@., $(COQPKGS)) -package @BIGINTPKG@
src/Plot/interval_plot.ml: src/Plot/plot.c
@CPP@ -DCOQVERSION=@COQVERSION@ $< -o $@
......
......@@ -36,6 +36,14 @@ if test "$COQVERSION" -lt 80800; then
fi
AC_MSG_RESULT($COQVERSION)
if test "$COQVERSION" -lt 81400; then
COQROOT=coq
else
COQROOT=coq-core
fi
AC_SUBST(COQROOT)
AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
AC_MSG_CHECKING([for coqdep])
if test ! "$COQDEP"; then
......@@ -148,7 +156,7 @@ if test "$native_tactic" = yes; then
AC_MSG_CHECKING([for native development files])
AS_IF(
[ echo "let _ = (Evd.empty, $BIGINTMOD.zero_big_int)" > conftest.ml
$OCAMLFIND ocamlopt -rectypes -thread -package coq.engine -package $BIGINTPKG -shared conftest.ml -o conftest.cmxs ],
$OCAMLFIND ocamlopt -rectypes -thread -package $COQROOT.engine -package $BIGINTPKG -shared conftest.ml -o conftest.cmxs ],
[ AC_MSG_RESULT(yes) ],
[ AC_MSG_RESULT(no)
AC_MSG_ERROR([ *** Failed to compile a native OCaml library ]) ])
......@@ -158,7 +166,7 @@ if test "$byte_tactic" = yes; then
AC_MSG_CHECKING([for bytecode development files])
AS_IF(
[ echo "let _ = (Evd.empty, $BIGINTMOD.zero_big_int)" > conftest.ml
$OCAMLFIND ocamlc -rectypes -thread -package coq.engine -package $BIGINTPKG -c conftest.ml -o conftest.cmo ],
$OCAMLFIND ocamlc -rectypes -thread -package $COQROOT.engine -package $BIGINTPKG -c conftest.ml -o conftest.cmo ],
[ AC_MSG_RESULT(yes) ],
[ AC_MSG_RESULT(no)
AC_MSG_ERROR([ *** Failed to compile a bytecode OCaml library ]) ])
......
......@@ -169,7 +169,7 @@ let () =
(Extend.TUentry (Genarg.get_arg_tag Stdarg.wit_constr),
Vernacextend.TyNil)),
#if COQVERSION >= 81400
(fun r ?loc ~atts ->
(fun r ?loc ~atts () ->
#else
(fun r ~atts ->
#endif
......@@ -188,7 +188,7 @@ let () =
(Extend.TUentry (Genarg.get_arg_tag Stdarg.wit_string),
Vernacextend.TyNil)))),
#if COQVERSION >= 81400
(fun r s ?loc ~atts ->
(fun r s ?loc ~atts () ->
#else
(fun r s ~atts ->
#endif
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment