aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-04-27Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Pierre-Marie Pédrot
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails.
2017-04-25Merge PR#567: Fix bug #5377: @? patterns broken.Maxime Dénès
2017-04-24Merge PR#577: Add bedrock targets src and facade to Travis CIMaxime Dénès
2017-04-20Add bedrock targets src and facadeJason Gross
2017-04-20Fix bug #5377: @? patterns broken.Pierre-Marie Pédrot
2017-04-19Merge PR#538: Correction of bug #4306Maxime Dénès
2017-04-14Fixing bug #5470 (anomaly on notations with misused "binder" type).Hugo Herbelin
2017-04-14Fixing bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
2017-04-14Fix EOL characters in xml protocol documentation.Maxime Dénès
2017-04-14Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.Maxime Dénès
2017-04-14Fix anomaly when doing [all:Check _.] during a proof.Gaetan Gilbert
2017-04-14Merge PR#563: add XML protocol doc for 8.6Maxime Dénès
2017-04-14[travis] Use the lite target for fiat-crypto.Maxime Dénès
2017-04-13update XML protocol doc to 8.6Paul Steckler
2017-04-13add XML protocol doc for 8.5Paul Steckler
2017-04-12Merge PR#510: Correctly identify [Time Defined.] as a definedMaxime Dénès
2017-04-08Fixing #5460 (limitation in computing deps in pattern-matching compilation).Hugo Herbelin
This was assuming dependencies occurring in configurations of the form x:A, y:B x, z:C x y |- match x, y, z with ... end". But still work to do for better management of dependencies in general...
2017-04-06Fix a few programming pearls related to Time, Fail and Redirect.Maxime Dénès
This fixes a few clear bugs, but the STM code handling Time, Fail and Redirect before par: still needs to be rewritten. It does not implement the same semantics as the vernac interpreter for Fail Fail [c] and ignores Redirect. This commit was already reviewed with Enrico and tested on Travis.
2017-04-06Merge branch 'origin/v8.5' into v8.6.Hugo Herbelin
Was needed to be done for a while.
2017-04-05Fixing #5454 (an assert false with 'pat).Hugo Herbelin
Note: Apparently not easy to make a test file as the error is raised in "G_vernac.fresh_var" at parsing time (not captured by Fail).
2017-04-04closing bug file for #4306Julien Forest
2017-04-04end of correction of bug 4306Julien Forest
2017-04-04Bad correction in previous commitJulien Forest
2017-04-04Solving first problem in bug #4306. TO DO : solve the let in problemJulien Forest
2017-04-04bug file for 4306Julien Forest
2017-04-04Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-04Test file for #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-04Fix bug #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously avoided by a safeguard I put in nativecode.ml. But other kernel changes in this commit should probably be reviewed carefully.
2017-04-03Merge PR#533: Instances should obey universe binders even when defined by ↵Maxime Dénès
tactics.
2017-04-03Instances should obey universe binders even when defined by tactics.Gaetan Gilbert
2017-04-03Add test file for #4957.Maxime Dénès
Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly".
2017-03-30Merge PR#463: Run non-tactic comands without resilient_commandMaxime Dénès
2017-03-29Merge PR#514: [travis] Backport from trunk: VSTMaxime Dénès
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
2017-03-24[travis] Backport from trunk: VSTEmilio Jesus Gallego Arias
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-23Correctly identify [Time Defined.] as a definedTej Chajed
Need to check inside control expressions. Also fixes handling of [Redirect "file" Defined.] and [Timeout n Defined.]. Fixes Coq bug 5411 (https://coq.inria.fr/bugs/show_bug.cgi?id=5411): coqc -quick hangs on [Time Defined.]
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#497: [travis] [8.6.only] Backport latest changes from trunk.Maxime 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-22Merge PR#480: show unused intro pattern warningMaxime Dénès
2017-03-22[travis] [8.6.only] Backport latest changes from trunk.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 18:40:44 +0000