aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-11-28Tactic primitives: missing [advance] lead to spurious dangling goals.Arnaud Spiwack
2014-11-28STM: if a-p-always-delegate fetch states from parked worker on edit-atEnrico Tassi
2014-11-28Future: API for blocking futuresEnrico Tassi
2014-11-27Reverting the following block of three commits:Hugo Herbelin
2014-11-27FAQ: fix some broken urlsPierre Letouzey
2014-11-27STM: hook called whenever a state is unreachableEnrico Tassi
2014-11-27typosEnrico Tassi
2014-11-27Fix test flags for fake_ideEnrico Tassi
2014-11-27better to always print the thread idEnrico Tassi
2014-11-27async_queries_* merged with async_proofs_*Enrico Tassi
2014-11-27AsyncTaskQueue: parsin can also happen in the workers nowEnrico Tassi
2014-11-27STM: new API async_queryEnrico Tassi
2014-11-27AsyncTaskQueue: API to park a workerEnrico Tassi
2014-11-27WorkerPool: API to move a worker from an active pool to a parking oneEnrico Tassi
2014-11-27TQueue: let reader be picky when popping an itemEnrico Tassi
2014-11-27STM: put hooks in key events to let plugins customize the feedbackEnrico Tassi
2014-11-27Feedback: API cleaned up, documented and made user extensibleEnrico Tassi
2014-11-26Fixing Coq compilation.Pierre-Marie Pédrot
2014-11-26Experimenting always forcing convertibility on strict implicit argumentsHugo Herbelin
2014-11-26Registering strict implicit arguments systematically.Hugo Herbelin
2014-11-25Bug #3804 is actually closed (thanks to Jason Gross for the notification).Xavier Clerc
2014-11-25Tweak some test cases.Xavier Clerc
2014-11-25Fix order of arguments in Extract Constant for Pos.compare_cont.Maxime Dénès
2014-11-25Adding tag output to references in Ppconstr.Pierre-Marie Pédrot
2014-11-25Used an evar name based on the local def name in "evar" tactic.Hugo Herbelin
2014-11-25A bit more information in debug tactic unification.Hugo Herbelin
2014-11-25Adapting to current semantics of "simpl non-evaluable-cst"Hugo Herbelin
2014-11-25Experimenting using unification when matching evar/meta free subtermsHugo Herbelin
2014-11-24Plugging console highlighting in for toplevel and compilation error messages.Pierre-Marie Pédrot
2014-11-24Adding test for bug #3248.Pierre-Marie Pédrot
2014-11-24Fixing bug #3817.Pierre-Marie Pédrot
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-11-23One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Hugo Herbelin
2014-11-23Add printer for transparent state for ocamldebug.Hugo Herbelin
2014-11-23Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc aboutHugo Herbelin
2014-11-23Fix #3824. de Bruijn error in normalization of fixpoints.Maxime Dénès
2014-11-22Specific printer of Evar.Set.t for ocamldebug + more information inHugo Herbelin
2014-11-22Attempt to organize and document unification flags of setoid rewrite.Hugo Herbelin
2014-11-22Removing superfluous newlines in setoid_rewrite error message.Hugo Herbelin
2014-11-22In setoid_rewrite error messages:Hugo Herbelin
2014-11-22Test for closed #2713 and #2876.Hugo Herbelin
2014-11-22Further simplifying functional induction.Hugo Herbelin
2014-11-22Simplifying code of functional induction.Hugo Herbelin
2014-11-22Not using an (arbitrary) pivot anymore for re-introduction ofHugo Herbelin
2014-11-22New simplification of code for generalizing hypotheses in destruct.Hugo Herbelin
2014-11-22Removing a hack which, according to the comment, should not be necessaryHugo Herbelin
2014-11-22Add test-suite file for dependent rewriting example by Vadim Zaliva andMatthieu Sozeau
2014-11-22Fix resolve_morphism to build well-scoped terms in case some argumentsMatthieu Sozeau
2014-11-22Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.Pierre-Marie Pédrot
2014-11-22Writing intro_replacing in the new monad.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 10:47:38 +0000