aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-04-01Declaring ltac plugin, so that static linking works.Hugo Herbelin
2017-03-30Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-30Merge PR#463: Run non-tactic comands without resilient_commandMaxime Dénès
2017-03-30Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Guillaume Melquiond
2017-03-30Merge PR#469: Added take to VectorDefMaxime Dénès
2017-03-30Added take to VectorDef.George Stelle
Added a function that takes the first [p] elements of a vector, and a few lemmas proving some of its properties.
2017-03-30Merge PR#511: [stm] Remove some obsolete vernacs/classification.Maxime Dénès
2017-03-29Merge PR#522: [coqide] Protect against size_allocate race in proofview.Maxime Dénès
2017-03-29Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-29Merge PR#514: [travis] Backport from trunk: VSTMaxime Dénès
2017-03-29Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.Maxime Dénès
2017-03-29Merge PR#521: Do so that "About" tells if a reference is a coercion.Maxime Dénès
2017-03-29Merge PR#525: [ide] Fix typo in pp serialization.Maxime Dénès
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
2017-03-29[ide] Fix typo in pp serialization.Emilio Jesus Gallego Arias
2017-03-28Fixing missing PropFacts.v in Logic/vo.itarget.Hugo Herbelin
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.
2017-03-28[coqide] Protect against size_allocate race in proofview.Emilio Jesus Gallego Arias
To handle dynamic printing in CoqIDE we listen to the `size_allocate` signal , [see more details in 6885a398229918865378ea24f07d93d2bcdd2802] However, we must be careful to protect against scrollbar creation: it is possible for the `size_allocate` handler to change the size when inserting text (due to scrollbars), thus we may enter in an infinite loop. Our fix is to check if the width has really changed, as done in `Wg_MessageView`. This fixes the problem noted by @herbelin in https://coq.inria.fr/bugs/show_bug.cgi?id=5417
2017-03-27Do so that "About" tells if a reference is a coercion.Hugo Herbelin
2017-03-24[travis] Backport from trunk: VSTEmilio Jesus Gallego Arias
2017-03-24Merge PR#489: [travis] Add VSTMaxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away.
2017-03-24[nit] Fix a couple incorrect uses of msg_error.Emilio Jesus Gallego Arias
2017-03-24[travis] Add VSTEmilio Jesus Gallego Arias
2017-03-24Merge PR#392: strengthened the statement of JMeq_eq_depMaxime Dénès
2017-03-24Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-24Merge PR#476: [future] Be eager when "chaining" already resolved future values.Maxime Dénès
2017-03-24Merge PR#475: Opaque side effectsMaxime Dénès
2017-03-24Merge PR#504: [META] add support for ide librariesMaxime Dénès
2017-03-23Merge PR#503: make check not CoqIDE-specificMaxime Dénès
2017-03-23Merge PR#433: doc: fix a French-ismMaxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#507: Intern names bound in match patternsMaxime Dénès
2017-03-23Documenting the API of side-effects.Pierre-Marie Pédrot
2017-03-23Using a dedicated datastructure for side effect ordering.Pierre-Marie Pédrot
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.
2017-03-23Making the side_effects type opaque.Pierre-Marie Pédrot
We move it from Entries to Term_typing and export the few functions needed to manipulate it in this module.
2017-03-23Intern names bound in match patternsTej Chajed
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345): Cannot use names bound in matches inside Ltac definitions.
2017-03-23Merge PR#501: [travis] Fix iris-coq build.Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.Maxime Dénès
2017-03-23Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Maxime Dénès
This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#495: funind: Ignore missing info for current functionMaxime Dénès
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
2017-03-23Merge PR#491: Do not typecheck twice the type of opaque constants.Maxime Dénès
2017-03-23[META] add support for ide librariesEmilio Jesus Gallego Arias
This makes sense for clients willing to link to richpp.
2017-03-22Merge PR#480: show unused intro pattern warningMaxime Dénès
2017-03-22Merge PR#493: [safe-string] update dev/doc/changesMaxime Dénès
2017-03-22Merge PR#415: Use a compact representation for real literalsMaxime Dénès
2017-03-22make check not CoqIDE-specificPaul Steckler
2017-03-22Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.Hugo Herbelin
This adds at least support for camlp5 6.14 (in addition to 6.17).
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:09:23 +0000