coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	coqdep: Warning about ml file clashes, keeping the file corresponding	Hugo Herbelin	2014-12-04
*	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	2014-12-03
*	When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if	Hugo Herbelin	2014-12-02
*	Postponing the "evar <= evar" problems instead of solving them in an	Hugo Herbelin	2014-12-02
*	Being more scrupulous on preserving subtyping in evar-evar problems.	Hugo Herbelin	2014-12-02
*	Being consistent in making arbitrary choices in recursive calls to	Hugo Herbelin	2014-12-02
*	Resolution of evar/evar problems: removed a test which should be	Hugo Herbelin	2014-12-02
*	For compatibility purpose, when setoid_rewriting a hypothesis, beta-iota	Pierre-Marie Pédrot	2014-12-02
*	More invariants in the code of Rewrite.	Pierre-Marie Pédrot	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-12-01
*	Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...	Hugo Herbelin	2014-11-30
*	Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.	Hugo Herbelin	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	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	2014-11-30
*	Adding missing unsafe primitives to Proofview.	Pierre-Marie Pédrot	2014-11-30
*	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	2014-11-28
*	Tactic primitives: missing [advance] lead to spurious dangling goals.	Arnaud Spiwack	2014-11-28
*	STM: if a-p-always-delegate fetch states from parked worker on edit-at	Enrico Tassi	2014-11-28
*	Future: API for blocking futures	Enrico Tassi	2014-11-28
*	Reverting the following block of three commits:	Hugo Herbelin	2014-11-27
*	FAQ: fix some broken urls	Pierre Letouzey	2014-11-27
*	STM: hook called whenever a state is unreachable	Enrico Tassi	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	2014-11-27
*	AsyncTaskQueue: API to park a worker	Enrico Tassi	2014-11-27
*	WorkerPool: API to move a worker from an active pool to a parking one	Enrico Tassi	2014-11-27
*	TQueue: let reader be picky when popping an item	Enrico Tassi	2014-11-27
*	STM: put hooks in key events to let plugins customize the feedback	Enrico Tassi	2014-11-27
*	Feedback: API cleaned up, documented and made user extensible	Enrico Tassi	2014-11-27
*	Fixing Coq compilation.	Pierre-Marie Pédrot	2014-11-26
*	Experimenting always forcing convertibility on strict implicit arguments	Hugo Herbelin	2014-11-26
*	Registering strict implicit arguments systematically.	Hugo Herbelin	2014-11-26
*	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