| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-11-25 | Fix order of arguments in Extract Constant for Pos.compare_cont. | Maxime Dénès | |
| 2014-11-25 | Adding tag output to references in Ppconstr. | Pierre-Marie Pédrot | |
| 2014-11-25 | Used an evar name based on the local def name in "evar" tactic. | Hugo Herbelin | |
| 2014-11-25 | A bit more information in debug tactic unification. | Hugo Herbelin | |
| 2014-11-25 | Adapting to current semantics of "simpl non-evaluable-cst" | Hugo Herbelin | |
| 2014-11-25 | Experimenting using unification when matching evar/meta free subterms | Hugo Herbelin | |
| while before these were supposed to consider only syntactically. Made the experiment to unify with all delta flags unset. Keeping the same flags as for non evar/meta free subterms would lead to too much successes, as e.g. "true && b" matching "b" when the modulo_conv_on_closed_terms flag is set, which is the case for rewrite. But maybe should we instead investigate to have the same flags but with the restrict_conv_on_strict_subterms flag set. This rules out examples like "true && b" unifying with "b" and this is another option which is ok for compiling the stdlib without any changes. | |||
| 2014-11-24 | Plugging console highlighting in for toplevel and compilation error messages. | Pierre-Marie Pédrot | |
| 2014-11-24 | Adding test for bug #3248. | Pierre-Marie Pédrot | |
| 2014-11-24 | Fixing bug #3817. | Pierre-Marie Pédrot | |
| Coqtop was wrongly assuming that receiving a SIGINT when reading on a channel meant that the channel was closed, resulting in a crash when interrupting an idle coqtop from CoqIDE. To prevent this, we block SIGINTs when reading in ide_slave. | |||
| 2014-11-23 | Pass around information on the use of template polymorphism for | Matthieu Sozeau | |
| inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821). | |||
| 2014-11-23 | One more word about "simpl f": avoid "simpl f" to be printed "simpl f", | Hugo Herbelin | |
| at least when f is an evaluable reference. | |||
| 2014-11-23 | Add printer for transparent state for ocamldebug. | Hugo Herbelin | |
| 2014-11-23 | Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc about | Hugo Herbelin | |
| when the arguments of a constructor can be moved at the place of the variable on which destruct or induction applies. | |||
| 2014-11-23 | Fix #3824. de Bruijn error in normalization of fixpoints. | Maxime Dénès | |
| This bug was affecting the VM and the native compiler, but only in the pretyper (not the kernel). Types of arguments of fixpoints were incorrectly normalized due to a missing lift. | |||
| 2014-11-22 | Specific printer of Evar.Set.t for ocamldebug + more information in | Hugo Herbelin | |
| a UserError to ease debugging. | |||
| 2014-11-22 | Attempt to organize and document unification flags of setoid rewrite. | Hugo Herbelin | |
| 2014-11-22 | Removing superfluous newlines in setoid_rewrite error message. | Hugo Herbelin | |
| 2014-11-22 | In setoid_rewrite error messages: | Hugo Herbelin | |
| - removed the encapsulation in a Tactic Failure (I don't see why setoid_rewrite should specifically raise a Fail - do I miss something?) - avoid having twice a "Unable to satisfy ... constraints" message. | |||
| 2014-11-22 | Test for closed #2713 and #2876. | Hugo Herbelin | |
| 2014-11-22 | Further simplifying functional induction. | Hugo Herbelin | |
| 2014-11-22 | Simplifying code of functional induction. | Hugo Herbelin | |
| 2014-11-22 | Not using an (arbitrary) pivot anymore for re-introduction of | Hugo Herbelin | |
| quantified hypothesis in functional induction. This has apparently no visible effect, probably because functional schemes do not have non-dependent hypothesis in their branches besides induction hypotheses which are anyway introduced at the top of the context. | |||
| 2014-11-22 | New simplification of code for generalizing hypotheses in destruct. | Hugo Herbelin | |
| 2014-11-22 | Removing a hack which, according to the comment, should not be necessary | Hugo Herbelin | |
| anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)". | |||
| 2014-11-22 | Add test-suite file for dependent rewriting example by Vadim Zaliva and | Matthieu Sozeau | |
| Daniel Schepler. | |||
| 2014-11-22 | Fix resolve_morphism to build well-scoped terms in case some arguments | Matthieu Sozeau | |
| of the function are dependent. | |||
| 2014-11-22 | Enforcing the non-normalization of evars in Tactics.get_next_hyp_position. | Pierre-Marie Pédrot | |
| 2014-11-22 | Writing intro_replacing in the new monad. | Pierre-Marie Pédrot | |
| 2014-11-22 | Removing useless flag of the historical move tactic. | Pierre-Marie Pédrot | |
| 2014-11-22 | Exporting a primitive allowing to run completely the tactic monad. | Pierre-Marie Pédrot | |
| 2014-11-21 | Adding test for bug #3326. | Pierre-Marie Pédrot | |
| 2014-11-21 | Adding test for bug #3424. | Pierre-Marie Pédrot | |
| 2014-11-21 | Cleaning up closed bugs in test-suite. | Pierre-Marie Pédrot | |
| 2014-11-21 | Writing Tactics.keep in the new monad. | Pierre-Marie Pédrot | |
| 2014-11-21 | Test for bug #3788. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |