gitlab.inria.fr / coqinterval/interval / commits
| SHA | Message | Author | Date | Stats |
|---|---|---|---|---|
| dcdffc06 | Remove some useless definitions. | Guillaume Melquiond <g****d@i****r> | 4 months ago | |
| ecb62482 | Make it explicit that the proof scripts depend on rewrite's goal ordering. | Guillaume Melquiond <g****d@i****r> | 4 months ago | |
| 95197825 | Adapt to https://github.com/math-comp/math-comp/pull/1545 |
Pierre Roux <p****x@o****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
6 months ago | |
| 11e25a93 | Make it explicit that the proof script depends on rewrite's goal ordering. | Guillaume Melquiond <g****d@i****r> | 6 months ago | |
| 82ec28d1 | Make it explicit when the proof scripts rely on the legacy goal ordering. | Guillaume Melquiond <g****d@i****r> | 6 months ago | |
| d8c6a832 | New release. | Guillaume Melquiond <g****d@i****r> | 6 months ago | |
| 48876601 | Ensure compatibility with 9.2. | Guillaume Melquiond <g****d@i****r> | 6 months ago | |
| 99b11d76 | Move remake.cpp out of the way. | Guillaume Melquiond <g****d@i****r> | 7 months ago | |
| edb2cb2e | Use a custom implementation of coqdep. | Guillaume Melquiond <g****d@i****r> | 7 months ago | |
| 4f721703 | Prevent Coqdep from polluting dependencies. | Guillaume Melquiond <g****d@i****r> | 11 months ago | |
| 8efb321a | New release. | Guillaume Melquiond <g****d@i****r> | about 1 year ago | |
| 5991c58f | Ensure compatibility with Rocq 9.1. | Guillaume Melquiond <g****d@i****r> | about 1 year ago | |
| 5c5e9dcd | New release. | Guillaume Melquiond <g****d@i****r> | about 1 year ago | |
| d7fc21dd | Avoid running the build-image job, if possible. | Guillaume Melquiond <g****d@i****r> | about 1 year ago | |
| 5218bea6 | Ensure compatibility with Rocq 9.0. | Guillaume Melquiond <g****d@i****r> | about 1 year ago | |
| 7aa6563a | merge Merge branch 'mc12' into 'master' | Pierre Roux <p****x@o****r> | over 1 year ago | |
| b3926903 | Improve MC 1/2 detection | Pierre Roux <p****x@o****r> | over 1 year ago | |
| 12b3cf1d | merge Merge branch 'mc1415' into 'master' | Pierre Roux <p****x@o****r> | over 1 year ago | |
| 9d83c280 | Adapt to https://github.com/math-comp/math-comp/pull/1415 | Pierre Roux <p****x@o****r> | over 1 year ago | |
| 14ddc002 | Adapt to Coquelicot 4. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| b4ed038e | Remove useless computation. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| c44746ee | Remove some useless definitions. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| 978ad2b3 | Remove useless lemma. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| 10502e72 | Remove useless lemmas. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| 49f521f7 | Remove useless hypothesis. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| f954d17a | Remove unused tactics. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| d977ad1d | Simplify proof. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| 7b3a0ac3 | Simplify proof. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| 67c36748 | Give a direct definition of le_lower and use F'.le in I.sqrt and I.sqr. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| b1693731 | New release. | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| c823cb77 | Reduce the amount of inference in tactics. | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| d8cf8e8e | Be more permissive when recognizing "u <= e /\ e <= v". | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| a9d77293 | Fix CI documentation. | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| a4ba8a8a | Tighten enclosure of exponential for inputs greater than 709.78. |
Paul Geneau de Lamarliere <p****e@i****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
almost 2 years ago | |
| 0f54076c | Prove the correctness of the lookup function. | Guillaume Melquiond <g****d@i****r> | about 2 years ago | |
| 8cef3276 | Update Docker image. | Guillaume Melquiond <g****d@i****r> | about 2 years ago | |
| d6a03b30 | Bump dependencies to comply with Coq >= 8.13 and clean files accordingly. | Guillaume Melquiond <g****d@i****r> | about 2 years ago | |
| 5f642217 | Simplify proof. | Guillaume Melquiond <g****d@i****r> | about 2 years ago | |
| 885fad7f | New release. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 38ba2cb0 | Make Coq 8.13.1 the minimal version. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| c7c6978f | Add some tests and documentation. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 0c32d3a0 | Work a bit harder to display types. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 15277128 | Experiment with some commands for pocket calculations. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 0cafdd63 | Make proofs a bit more generic. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 0d988623 | Strengthen bounds a bit. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| dedc3163 | Teach interval about F2R. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 8b332be1 | Inline proofs and simplify them. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| e4f15529 | Make remove_float a degenerate form of assert_float. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| bd6cdeec | Rename to assert_float, add remove_float, and simplify proofs. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| ad05705d | Make simplify_wb fail instead of letting it ask for a proof of False. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 6512fda4 | Linearize proof a bit. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| a84834cc | Merge intermediate lemma into the main proof. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| dc980a03 | Add a tactic assert_float_transparent. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 8c7a5c04 | New release. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| b896979d | Add a variant of SF2B a bit easier to use. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 559c6a54 | Simplify proofs a bit. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| b47f25cc | Factor proof a bit. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 144942b0 | Add support for integers to remove_floats. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 3c14ea3b | Improve remove_floats. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 33dd1653 | Merge lemma about argument reduction and remove some useless definitions. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| f49ae518 | Hide types better and remove some useless definitions. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| df44bcad | Simplify proof a bit. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| a8b18e81 | Fix compilation of plugin with Coq 8.19. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| e41f3aa2 | Avoid inefficiency with Coq 8.19. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 775927c7 | Adapt to Coq 8.19 |
Pierre Roux <p****x@o****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 2 years ago | |
| d0e677dc | Enable the optimized primitives only if the language of expression is available. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 8dd07368 | Add an interval version of the primitive exponential. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| ef82328d | Implement a primitive version of exponential. |
Paul Geneau de Lamarliere <p****e@i****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 2 years ago | |
| 80e91def | Clean a bit. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| a94a0ede | Import changes to the language of expressions. |
Paul Geneau de Lamarliere <p****e@i****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 2 years ago | |
| 1cf37203 | Support "u <= e < v" and other variations as goals. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| af37529b | Prove a slightly stronger version of F.div_DN_correct. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| fb113c91 | Prove a slightly stronger version of F.div_UP_correct. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 96160a5c | Prove a slightly stronger version of F.mul_DN_correct. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| e2bc61b1 | merge Merge branch 'coq819' into 'master' | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| cab8daf8 | Adapt to Coq 8.19 | Pierre Roux <p****x@o****r> | over 2 years ago | |
| cccb6b55 | Prove a slightly stronger version of F.mul_UP_correct. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 928e8fbc | Give a slightly better statement to B2R_BtoX. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 6506ad3a | Factor proof about PI/2. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 7aeaab59 | Avoid indirection. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| abea12d0 | Remove dependency. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 56a2e46e | Silence warning about duplicate clears. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 8dc131f4 | Remove lemmas from the standard library. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 8f235aaf | New release. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| c2fa060e | merge Merge branch 'mc_1110' into 'master' | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 453cb586 | Adapt to https://github.com/math-comp/math-comp/pull/1110 | Pierre Roux <p****x@o****r> | almost 3 years ago | |
| e3cfdedb | Add an internal notation for the interval tactic. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| db982c7c | Fix pessimization in PI's upper bound. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| cf181109 | Simplify handling of dummy values. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| bca5b847 | Handle fixed-point rounding. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 45f9b2cb | Add an enclosure for fixed-point errors. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| d068ee63 | Factor out the definition of elementary rounding errors. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| c40542dc | Prevent unfolding of supported binary operators. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 726de026 | Recognize elementary rounding errors as a unary operator. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 7f433748 | Use a tighter bound for error_flt. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| f25cdd34 | Add a specification for F.mag. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 672a174a | New release. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| fd04a57a | Improve error messages for integral_intro. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 7dc9e877 | Avoid spurious failure when looking for hypotheses. | Guillaume Melquiond <g****d@i****r> | about 3 years ago | |
| 0dadda85 | Remove custom check for Plot. | Guillaume Melquiond <g****d@i****r> | about 3 years ago |