aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-29 15:35:18 +0000