| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-08-19 | Split ConstructiveRealsLUB and improve comments | Vincent Semeria | |
| 2019-08-10 | Compute (if linear_order_T 0 (IPR 22) (IPR 10) (IPR_pos 10) then true else ↵ | Vincent Semeria | |
| false). | |||
| 2019-08-09 | Switch constructive Rlt to sort Type, to make it compute later | Vincent Semeria | |
| 2019-08-08 | Fix namespace of Cauchy reals | Vincent Semeria | |
| 2019-08-08 | Add interface of constructive real numbers, with an opaque implementation by ↵ | Vincent Semeria | |
| Cauchy reals | |||
| 2019-08-06 | Prove the completeness of real numbers from logical axiom sig_not_dec | Vincent Semeria | |
| 2019-08-05 | Merge PR #10445: Split constructive and classical axioms for real numbers | Vincent Laporte | |
| Ack-by: Zimmi48 Ack-by: silene | |||
| 2019-08-05 | ConstructiveCauchyReals: make explicit structural recursion | Vincent Laporte | |
| 2019-07-26 | Fix typo | Vincent Semeria | |
| 2019-07-24 | changed name of cos3PI4 to cos_3PI4 for consistency | Robert Rand | |
| 2019-07-17 | Rename ConstructiveRIneq and ConstructiveRcomplete | Vincent Semeria | |
| 2019-07-16 | Define constructive real numbers as Cauchy sequences of rational numbers. ↵ | Vincent Semeria | |
| Redefine classical real numbers as a quotient of those constructive real numbers. | |||
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2019-05-23 | Fixing typos - Part 3 | JPR | |
| 2019-05-23 | Fixing typos - Part 3 | JPR | |
| 2019-05-07 | Improve field_simplify on fractions with constant denominator | thery | |
| Before this patch, `x` was "simplified" to `x / 1`. | |||
| 2019-04-01 | Several improvements and fixes of Lia | Frédéric Besson | |
| - Improved reification for Micromega (support for #8764) - Fixes #9268: Do not take universes into account in lia reification Improve #9291 by threading the evar_map during reification. Universes are unified. - Remove (potentially cyclic) dependency over lra for Rle_abs - Towards a complete simplex-based lia fixes #9615 Lia is now exclusively using cutting plane proofs. For this to always work, all the variables need to be positive. Therefore, lia is pre-processing the goal for each variable x it introduces the constraints x = y - z , y>=0 , z >= 0 for some fresh variable y and z. For scalability, nia is currently NOT performing this pre-processing. - Lia is using the FSet library manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4 to work around a "leaked" hint breaking compatibility of eauto | |||
| 2019-03-30 | Error when [foo.(bar)] is used with nonprojection [bar] | Gaëtan Gilbert | |
| (warn if bar is a nonprimitive projection) | |||
| 2018-12-19 | Put #[universes(template)] on all auto template spots in stdlib | Gaëtan Gilbert | |
| 2018-11-19 | Merge PR #8987: Deprecate hint declaration/removal with no specified database | Pierre-Marie Pédrot | |
| 2018-11-14 | Deprecate hint declaration/removal with no specified database | Maxime Dénès | |
| Previously, hints added without a specified database where implicitly put in the "core" database, which was discouraged by the user manual (because of the lack of modularity of this approach). | |||
| 2018-11-01 | develop constructive epsilon | Vincent Semeria | |
| 2018-11-01 | Fix header and doc index | Vincent Semeria | |
| 2018-11-01 | proof that R is uncountable | Vincent Semeria | |
| 2018-09-10 | Declaring Scope prior to loading primitive printers. | Hugo Herbelin | |
| 2018-09-10 | Adapting standard library to the introduction of "Declare Scope". | Hugo Herbelin | |
| Removing in passing two Local which are no-ops in practice. | |||
| 2018-08-22 | Fix typo of caracterisation -> c*h*aracterisation | Siddharth Bhat | |
| 2018-07-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-03-08 | Merge PR #6909: Deprecate Focus and Unfocus | Maxime Dénès | |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-03-04 | Remove all uses of Focus in standard library. | Théo Zimmermann | |
| 2018-03-02 | Turn warning for deprecated notations on. | Théo Zimmermann | |
| Fix new deprecation warnings in the standard library. | |||
| 2018-02-28 | Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas | Maxime Dénès | |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2017-09-06 | weakens an hypothesis of Rle_Rpower | Yves Bertot | |
| 2017-09-06 | changed statements of Rpower_lt and Rle_power and added | Yves Bertot | |
| Rlt_Rpower_l and pow_INR. Unfortunately theorems Rpower_lt and Rle_power are named inconsistently, in spite of their similarity. | |||
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-14 | Remove deprecated options from the standard library. | Guillaume Melquiond | |
| 2017-06-01 | drop vo.itarget files and compute the corresponding the corresponding values ↵ | Matej Kosik | |
| automatically instead | |||
| 2017-04-29 | Suppress warning message in stdlib. | Guillaume Melquiond | |
| 2017-04-27 | Merge PR#414: Some more theory on powerRZ. | Maxime Dénès | |
| 2017-04-07 | Add some hints to the "real" database to automatically discharge literal ↵ | Guillaume Melquiond | |
| comparisons. | |||
| 2017-04-02 | Fix documentation typo (bug #5433). | Guillaume Melquiond | |
| 2017-04-02 | Simplify some proofs. | Guillaume Melquiond | |
| This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing. | |||
| 2017-03-30 | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | Guillaume Melquiond | |
| 2017-03-22 | Make IZR a morphism for field. | Guillaume Melquiond | |
| There are now two field structures for R: one in RealField and one in RIneq. The first one is used to prove that IZR is a morphism which is needed to define the second one. | |||
| 2017-03-22 | Change the parser and printer so that they use IZR for real constants. | Guillaume Melquiond | |
| There are two main issues. First, (-cst)%R is no longer syntactically equal to (-(cst))%R (though they are still convertible). This breaks some rewriting rules. Second, the ring/field_simplify tactics did not know how to refold real constants. This defect is no longer hidden by the pretty-printer, which makes these tactics almost unusable on goals containing large constants. This commit also modifies the ring/field tactics so that real constant reification is now constant time rather than linear. Note that there is now a bit of code duplication between z_syntax and r_syntax. This should be fixed once plugin interdependencies are supported. Ideally the r_syntax plugin should just disappear by declaring IZR as a coercion. Unfortunately the coercion mechanism is not powerful enough yet, be it for parsing (need the ability for a scope to delegate constant parsing to another scope) or printing (too many visible coercions left). | |||
| 2017-03-22 | Make IZR use a compact representation of integers. | Guillaume Melquiond | |
| That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means that, after reduction, real constants no longer exponentially blow up. Note that I was not able to fix the test-suite for the declarative mode, so the missing proof terms have been admitted. | |||
| 2017-03-22 | Simplify some proofs using ring and field. | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |