aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | For now we only normalize sorts, and we leave instances for the next commit.
* Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
|
* Ensuring proper cast invariants in EConstr.kind.Gravatar Pierre-Marie Pédrot2017-03-31
| | | | | | The kernel does fishy things with casts, such that ensuring there are no two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr view as well.
* Revert "Specially crafted EConstr.kind to be more efficient."Gravatar Pierre-Marie Pédrot2017-03-31
| | | | | This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance difference was not conclusive enough to pay for the code ugliness.
* Specially crafted EConstr.kind to be more efficient.Gravatar Pierre-Marie Pédrot2017-03-30
| | | | | We do one step of loop unrolling, limit the number of allocations and mark the function as inline.
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-29
|\
* | Fix call to broken unsafe_type_of in apply tactic.Gravatar Maxime Dénès2017-03-29
| | | | | | | | | | This broke the build of iris-coq in the EConstr branch. Each time you use unsafe_type_of, I loose a night of sleep, so please stop.
* | Revert to incorrect heuristic in apply.Gravatar Maxime Dénès2017-03-28
| | | | | | | | Was breaking e.g. fiat-crypto.
| * Fixing missing PropFacts.v in Logic/vo.itarget.Gravatar Hugo Herbelin2017-03-28
| | | | | | | | | | | | This is while waiting for a possible different solution, if ever such a different solution is adopted, since the coq.inria.fr/library has currently a broken link and someone rightly complained about it.
* | Mathcomp overlay.Gravatar Maxime Dénès2017-03-25
| |
* | Fix interpretation of Ltac patterns episode 2.Gravatar Maxime Dénès2017-03-24
| | | | | | | | | | | | | | After 5db9588098f9f, some extra evar-normalization remained (compared to trunk) that would change the semantics e.g. of change bindings under Ltac match. This is just circumventing a fundamental flaw in the treatment of patterns.
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\|
| * Merge PR#489: [travis] Add VSTGravatar Maxime Dénès2017-03-24
| |\
| | * [travis] Add VSTGravatar Emilio Jesus Gallego Arias2017-03-24
| | |
| * | Merge PR#392: strengthened the statement of JMeq_eq_depGravatar Maxime Dénès2017-03-24
| |\ \
| * \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-24
| |\ \ \
| | * \ \ Merge PR#476: [future] Be eager when "chaining" already resolved future values.Gravatar Maxime Dénès2017-03-24
| | |\ \ \
| | * \ \ \ Merge PR#475: Opaque side effectsGravatar Maxime Dénès2017-03-24
| | |\ \ \ \
| * | \ \ \ \ Merge PR#504: [META] add support for ide librariesGravatar Maxime Dénès2017-03-24
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge PR#503: make check not CoqIDE-specificGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge PR#433: doc: fix a French-ismGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|/ | |/| | | | | | |
| * | | | | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \ | | | |_|_|/ / / / | | |/| | | | | |
| | * | | | | | | Merge PR#507: Intern names bound in match patternsGravatar Maxime Dénès2017-03-23
| | |\ \ \ \ \ \ \
| | | | | | | * | | Documenting the API of side-effects.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | |
| | | | | | | * | | Using a dedicated datastructure for side effect ordering.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We were doing fishy things in the Term_typing file, where side-effects were not considered in the right uniquization order because of the uniq_seff_rev function. It probably did not matter after a9b76df because effects were (mostly) uniquize upfront, but this is not clear because of the use of the transparente API in the module. Now everything has to go through the opaque API, so that a proper dependence order is ensured.
| | | | | | | * | | Making the side_effects type opaque.Gravatar Pierre-Marie Pédrot2017-03-23
| | | |_|_|_|/ / / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move it from Entries to Term_typing and export the few functions needed to manipulate it in this module.
| | | * | | | | | Intern names bound in match patternsGravatar Tej Chajed2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345): Cannot use names bound in matches inside Ltac definitions.
| * | | | | | | | Merge PR#501: [travis] Fix iris-coq build.Gravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \ \ | | | |/ / / / / / / | | |/| | | | | | |
| | * | | | | | | | Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.Gravatar Maxime Dénès2017-03-23
| | |\ \ \ \ \ \ \ \
| * | | | | | | | | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
| * | | | | | | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\| | | | | | | | |
| | * | | | | | | | | Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
| | |\ \ \ \ \ \ \ \ \ | | | |_|_|/ / / / / / | | |/| | | | | | | |
| | * | | | | | | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
| | * | | | | | | | | Merge PR#491: Do not typecheck twice the type of opaque constants.Gravatar Maxime Dénès2017-03-23
| | |\ \ \ \ \ \ \ \ \
| | | | | | | | | * | | [META] add support for ide librariesGravatar Emilio Jesus Gallego Arias2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes sense for clients willing to link to richpp.
| | * | | | | | | | | | Merge PR#480: show unused intro pattern warningGravatar Maxime Dénès2017-03-22
| | |\ \ \ \ \ \ \ \ \ \
| * | \ \ \ \ \ \ \ \ \ \ Merge PR#493: [safe-string] update dev/doc/changesGravatar Maxime Dénès2017-03-22
| |\ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#415: Use a compact representation for real literalsGravatar Maxime Dénès2017-03-22
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * | | | make check not CoqIDE-specificGravatar Paul Steckler2017-03-22
| | | | | | | | | | | |/ / /
| * | | | | | | | | | / / / Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.Gravatar Hugo Herbelin2017-03-22
| | |_|_|_|_|_|_|_|_|/ / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This adds at least support for camlp5 6.14 (in addition to 6.17).
| | | | | | | | | * | | | [travis] Fix iris-coq build.Gravatar Emilio Jesus Gallego Arias2017-03-22
| | |_|_|_|_|_|_|/ / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We need to do a bit of hacking, but it should be fine for the short term. c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83
| | * | | | | | | | | | Document the changes to IZR.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | |
| | * | | | | | | | | | Make IZR a morphism for field.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | | | | | | | Mark ring morphisms as opaque.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This prevents Coq from unfolding IZR in ring_simplify and field_simplify. This is a change of behavior for users of morphism rings, so they might have to pass the postprocess option to Add Ring/Field if they want morphisms to be automatically expanded. There are two predefined morphisms in the standard library: IDphi (when polynomial coefficients have the same type as constants) and gen_phiZ (when the only available constants are 0 and 1). They are hardcoded as transparent.
| | * | | | | | | | | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| | | | | | | | * | | | [travis] [8.6.only] Backport latest changes from trunk.Gravatar Emilio Jesus Gallego Arias2017-03-22
| | | | | |_|_|/ / / / | | | | |/| | | | | |
| | * | | | | | | | | Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | | | | | | Fix broken evaluation strategies for ring and field.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A bang indicates an argument that must be reduced, a star indicates an argument that must be handled recursively. PEeval: R r0 r1 add mul sub opp C phi Cpow powphi pow varmap pol 0 1 2 3 4 5 6 7 8! 9 10! 11 12* 13! FEeval: R r0 r1 add mul sub opp div inv C phi Cpow powphi pow varmap pol 0 1 2 3 4 5 6 7 8 9 10! 11 12! 13 14* 15! Pphi_dev: R r0 r1 add mul sub opp C c0 c1 ceq phi sign varmap pol 0 1 2 3 4 5 6 7 8! 9! 10! 11! 12! 13* 14! Pphi_pow: R r0 r1 add mul sub opp C c0 c1 ceq phi Cpow powphi pow sign varmap pol 0 1 2 3 4 5 6 7 8! 9! 10! 11! 12 13! 14 15! 16* 17! display_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi sign varmap num den 0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13! 14* 15! 16! display_pow_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi Cpow powphi pow sign varmap num den 0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13 14! 15 16! 17* 18! 19! PCond: R r0 r1 add mul sub opp eq C phi Cpow powphi pow varmap pol 0 1 2 3 4 5 6 7 8 9! 10 11! 12 13* 14!
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 02:12:10 +0000