aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Using the same type of binders for interning and externing.Gravatar Hugo Herbelin2017-03-24
| | | | | | Previously a union type was used for externing. In particular, moving extended_glob_local_binder to glob_constr.ml.
* Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | RawLocal -> CLocal
* Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | This is a bit long, but it is to keep a symmetry with constr_expr.
* Merging glob_binder and glob_decl.Gravatar Hugo Herbelin2017-03-24
|
* Type extended_glob_local_binder now contains only glob_constr.Gravatar Hugo Herbelin2017-03-24
| | | | No more constr_expr in it.
* Standardized the order of constructors for binders: Assum then Def.Gravatar Hugo Herbelin2017-03-24
|
* Cleaning phase around local binder at glob level:Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | Aligned the type binder_data to the naming scheme used in (raw) local_binder and Rel.Declaration.t. Made some code factorization. Still to do: align type Glob_term.glob_binder to the Assum/Def format too. Note: this includes fix of anomaly with 'pat in cofix (dec77f282).
* "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-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!
| * | | | | | | | | Fix some typos.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | |
| * | | | | | | | | Simplify some proofs using ring and field.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | |
| * | | | | | | | | Remove duplicate lemmas.Gravatar Guillaume Melquiond2017-03-22
|/ / / / / / / / /
| | | | | * / / / funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| | | |_|/ / / / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372) "Anomaly: Not a valid information when defining mutual fixpoints that are not mutual with Function".
* | | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
|\ \ \ \ \ \ \ \ | | |/ / / / / / | |/| | | | | |
* | | | | | | | Merge PR#390: Updates to the Pretty Printing InfrastructureGravatar Maxime Dénès2017-03-22
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#478: Small optimization on handling of library state.Gravatar Maxime Dénès2017-03-22
|\ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 09:19:49 +0000