aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-12-04coqdep: granting #2506 (./dir is the same as dir)Hugo Herbelin
2014-12-04coqdep: Warning about ml file clashes, keeping the file correspondingHugo Herbelin
2014-12-03Slight improving of a unification error message.Hugo Herbelin
2014-12-03Updading test-suite.Hugo Herbelin
2014-12-03In solve_evar_evar, orient the heuristic over arities with differentHugo Herbelin
2014-12-02When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifHugo Herbelin
2014-12-02Postponing the "evar <= evar" problems instead of solving them in anHugo Herbelin
2014-12-02Being more scrupulous on preserving subtyping in evar-evar problems.Hugo Herbelin
2014-12-02Being consistent in making arbitrary choices in recursive calls toHugo Herbelin
2014-12-02Resolution of evar/evar problems: removed a test which should beHugo Herbelin
2014-12-02For compatibility purpose, when setoid_rewriting a hypothesis, beta-iotaPierre-Marie Pédrot
2014-12-01More invariants in the code of Rewrite.Pierre-Marie Pédrot
2014-12-01Fixing test-suite.Pierre-Marie Pédrot
2014-12-01Added an arithmetical characterization of the hypothesis of WKL.Hugo Herbelin
2014-12-01Remove dead codeEnrico Tassi
2014-12-01Better commentEnrico Tassi
2014-11-30Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...Hugo Herbelin
2014-11-30Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Hugo Herbelin
2014-11-30Documenting the Set Refine Instance Mode.Pierre-Marie Pédrot
2014-11-30Adding a Refine Instance Mode option that allows to deactivate thePierre-Marie Pédrot
2014-11-30Adding test for bug #3417.Pierre-Marie Pédrot
2014-11-30Test for bug #3485.Pierre-Marie Pédrot
2014-11-30Fixing printing of dirpathes in Ppconstr. It was reversed.Pierre-Marie Pédrot
2014-11-30Test for bug #3487.Pierre-Marie Pédrot
2014-11-30Test of bug #3682.Pierre-Marie Pédrot
2014-11-30Fixing bug #3682.Pierre-Marie Pédrot
2014-11-30Adding missing unsafe primitives to Proofview.Pierre-Marie Pédrot
2014-11-28fix compilation on ocaml 3.12 (Close: 3833)Enrico Tassi
2014-11-28Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.Arnaud Spiwack
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 01:11:47 +0000