Commit e6475e6b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'interval-3.4'

parents 8e72f379 3f9e20fe
Version 3.4.1
-------------
* ensured compatibility from Coq 8.7 to 8.10
Version 3.4.0
-------------
......
......@@ -9,6 +9,19 @@ This package is free software; you can redistribute it and/or modify it
under the terms of CeCILL-C Free Software License (see the [COPYING](COPYING) file).
Main author is Guillaume Melquiond <guillaume.melquiond@inria.fr>.
See the file [INSTALL.md](INSTALL.md) for installation instructions.
Project Home
------------
Homepage: http://coq-interval.gforge.inria.fr/
Repository: https://gitlab.inria.fr/coqinterval/interval
Bug tracker: https://gitlab.inria.fr/coqinterval/interval/issues
Invocation
----------
......
AC_INIT([Interval], [3.4.0],
AC_INIT([Interval], [3.4.1],
[Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[interval])
......@@ -79,7 +79,7 @@ AS_IF(
rm -f conftest.v conftest.vo conftest.err
if test "$libdir" = '${exec_prefix}/lib'; then
libdir="`$COQC -where`/user-contrib/Interval"
libdir="`$COQC -where | tr -d '\r' | tr '\\\\' '/'`/user-contrib/Interval"
fi
AC_MSG_NOTICE([building remake...])
......
......@@ -218,7 +218,7 @@ assert (Hexit : forall k powu ft,
apply Un_cv_atanc.
lra.
unfold atanc.
case in_int ; intros Hx.
case Ratan.in_int ; intros Hx.
case atanc_exists ; simpl projT1 ; intros l C.
exact C.
elim Hx.
......@@ -502,7 +502,7 @@ assert (Hexit : forall k powu ft,
apply Un_cv_atanc.
lra.
unfold atanc.
case in_int ; intros Hx.
case Ratan.in_int ; intros Hx.
case atanc_exists ; simpl projT1 ; intros l C.
exact C.
elim Hx.
......
......@@ -1203,7 +1203,7 @@ Proof.
intros Heq Hb Hd.
apply (Rmult_eq_reg_r (b * d)).
field_simplify; trivial.
now rewrite Heq.
try now rewrite Heq.
now apply Rmult_neq0.
Qed.
......
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