| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-04 | coqdep: Warning about ml file clashes, keeping the file corresponding | Hugo Herbelin | |
| to the first -I option. Fortunately, with -I option, only one file can be found by occurrence of the option, so on the contrary of -Q/-R options for v files, the order is not file-system dependent. | |||
| 2014-12-03 | Slight improving of a unification error message. | Hugo Herbelin | |
| 2014-12-03 | Updading test-suite. | Hugo Herbelin | |
| 2014-12-03 | In solve_evar_evar, orient the heuristic over arities with different | Hugo Herbelin | |
| types as it was before commit 710bae2a8c81a44. There is still at least one problem with bug #3392 to solve. | |||
| 2014-12-02 | When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if | Hugo Herbelin | |
| possible, which is the "natural" way to orient an equation. At least it matters for matching subterms against patterns, so that it is the pattern variables which are substituted if ever the subterm has itself existential variables, as in: Goal exists x, S x = x. eexists. destruct (S _). | |||
| 2014-12-02 | Postponing the "evar <= evar" problems instead of solving them in an | Hugo Herbelin | |
| arbitrary direction as if it were an "evar = evar" problem. | |||
| 2014-12-02 | Being more scrupulous on preserving subtyping in evar-evar problems. | Hugo Herbelin | |
| Incidentally, this allows to make earlier the collapse of CUMUL to CONV when force is true. | |||
| 2014-12-02 | Being consistent in making arbitrary choices in recursive calls to | Hugo Herbelin | |
| evar_define. Interestingly, the added choose in evarconv.ml allows solve_evar_evar to be observationally commutative, in the sense of not either fail or succeed in compiling the stdlib whether problems are given in the left-to-right or right-to-left order. | |||
| 2014-12-02 | Resolution of evar/evar problems: removed a test which should be | Hugo Herbelin | |
| subsumed by the call to project_evar_on_evar. | |||
| 2014-12-02 | For compatibility purpose, when setoid_rewriting a hypothesis, beta-iota | Pierre-Marie Pédrot | |
| normalize it afterwards. | |||
| 2014-12-01 | More invariants in the code of Rewrite. | Pierre-Marie Pédrot | |
| In particular, the old hypinfo is made as a proper cache, preventing dynamic tricks to decide whether it was rightful to refresh it. | |||
| 2014-12-01 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2014-12-01 | Added an arithmetical characterization of the hypothesis of WKL. | Hugo Herbelin | |
| 2014-12-01 | Remove dead code | Enrico Tassi | |
| 2014-12-01 | Better comment | Enrico Tassi | |
| 2014-11-30 | Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ↵ | Hugo Herbelin | |
| env. | |||
| 2014-11-30 | Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too. | Hugo Herbelin | |
| This allows to have the example in test setoid_unif.v to work again. | |||
| 2014-11-30 | Documenting the Set Refine Instance Mode. | Pierre-Marie Pédrot | |
| 2014-11-30 | Adding a Refine Instance Mode option that allows to deactivate the | Pierre-Marie Pédrot | |
| automatic refinement of instances, thus failing when provided with an incomplete term instead of silently lauching the proof mode. | |||
| 2014-11-30 | Adding test for bug #3417. | Pierre-Marie Pédrot | |
| 2014-11-30 | Test for bug #3485. | Pierre-Marie Pédrot | |
| 2014-11-30 | Fixing printing of dirpathes in Ppconstr. It was reversed. | Pierre-Marie Pédrot | |
| 2014-11-30 | Test for bug #3487. | Pierre-Marie Pédrot | |
| 2014-11-30 | Test of bug #3682. | Pierre-Marie Pédrot | |
| 2014-11-30 | Fixing bug #3682. | Pierre-Marie Pédrot | |
| The function initializing proofviews were marking all evars as non-resolvables for the proofview, while only goal evars ought to be. | |||
| 2014-11-30 | Adding missing unsafe primitives to Proofview. | Pierre-Marie Pédrot | |
| 2014-11-28 | fix compilation on ocaml 3.12 (Close: 3833) | Enrico Tassi | |
| 2014-11-28 | Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf. | Arnaud Spiwack | |
| When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening. Fixes test-suite/success/apply.v | |||
| 2014-11-28 | Tactic primitives: missing [advance] lead to spurious dangling goals. | Arnaud Spiwack | |
| Closes #3801. | |||
| 2014-11-28 | STM: if a-p-always-delegate fetch states from parked worker on edit-at | Enrico Tassi | |
| If the async-proofs-always-delegate is passed, workers are killed only when the proof they computed is obsolete. If one jumps back to a state that was computed by the worker (and not the master) instead of (re)computing such state in the master ask the worker to send it back. | |||
| 2014-11-28 | Future: API for blocking futures | Enrico Tassi | |
| 2014-11-27 | Reverting the following block of three commits: | Hugo Herbelin | |
| - Registering strict implicit arguments systematically (35fc7d728168) - Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6) - Fixing Coq compilation (894a3d16471) Systematically computing strict implicit arguments can lead to big computations, so I suspend this attempt, waiting for improved computation of implicit arguments, or alternative heuristics going toward having more conversion in rewrite. | |||
| 2014-11-27 | FAQ: fix some broken urls | Pierre Letouzey | |
| 2014-11-27 | STM: hook called whenever a state is unreachable | Enrico Tassi | |
| Even indirectly, if it depends on another state that in turn failed. | |||
| 2014-11-27 | typos | Enrico Tassi | |
| 2014-11-27 | Fix test flags for fake_ide | Enrico Tassi | |
| 2014-11-27 | better to always print the thread id | Enrico Tassi | |
| 2014-11-27 | async_queries_* merged with async_proofs_* | Enrico Tassi | |
| 2014-11-27 | AsyncTaskQueue: parsin can also happen in the workers now | Enrico Tassi | |
| 2014-11-27 | STM: new API async_query | Enrico Tassi | |
| When async_proofs_always_delegate is on, park proof workers and dispatch to them queries. This flips the current way of printing goals in PIDE base UIs: it is not the worker that prints all goals while coomputing the states (and the dies), it is the UI that asks for them when they are under the eyes of the user. | |||
| 2014-11-27 | AsyncTaskQueue: API to park a worker | Enrico Tassi | |
| Generalize the old model by letting one park a worker and by letting the (parked) worker be picky about the tasks it picks up. The use of that is the following: a proof worker, while performing its "main" task (building a proof term) computes all the intermediate states but returns only its main result. One can ask the worker to hang around, and react to special tasks, like printing the goals of an intermediate state. | |||
| 2014-11-27 | WorkerPool: API to move a worker from an active pool to a parking one | Enrico Tassi | |
| This lets me have a pool of active workers of a fixed size, plus a parking area where workers that completed their job can stay holding their state (and eventually one can ask them to query such state afterwards). | |||
| 2014-11-27 | TQueue: let reader be picky when popping an item | Enrico Tassi | |
| E.g. let a worker pick up only jobs he is able to deal with. | |||
| 2014-11-27 | STM: put hooks in key events to let plugins customize the feedback | Enrico Tassi | |
| The default hook value is the one used by CoqIDE | |||
| 2014-11-27 | Feedback: API cleaned up, documented and made user extensible | Enrico Tassi | |
| 2014-11-26 | Fixing Coq compilation. | Pierre-Marie Pédrot | |
| 2014-11-26 | Experimenting always forcing convertibility on strict implicit arguments | Hugo Herbelin | |
| in tactic unification. | |||
| 2014-11-26 | Registering strict implicit arguments systematically. | Hugo Herbelin | |
| 2014-11-25 | Bug #3804 is actually closed (thanks to Jason Gross for the notification). | Xavier Clerc | |
| 2014-11-25 | Tweak some test cases. | Xavier Clerc | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |