aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-04-02A debug printer for Evd.Filter.tPierre Boutillier
2014-04-02Add a test case for bug 3251Jason Gross
2014-04-02STM: be more resilient to explicit Back + Sideff commands (closes: 3251)Enrico Tassi
2014-04-02Fix Bug 3131 + Really drop mentions of info in refman.Pierre Boutillier
2014-04-02Fix Bug 3217Pierre Boutillier
2014-04-02Better error message when found more than once object of name ...Pierre Boutillier
2014-04-01Evars introduced by Proofview refining are flagged as GoalEvar. For somePierre-Marie Pédrot
2014-04-01Updated debugging printersHugo Herbelin
2014-04-01Propagating conversion_problem towards (postponed) evar/evar problems.Hugo Herbelin
2014-04-01Fixing bug #2900 (evar/evar unif was supposed to be treated inHugo Herbelin
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-31Removing dead code in Tactics.Pierre-Marie Pédrot
2014-03-28Using the new refine interface to define ML tactics.Pierre-Marie Pédrot
2014-03-28Lighter interface for creating refining tactics.Pierre-Marie Pédrot
2014-03-28Newline on -slash warning in coqdep.Pierre-Marie Pédrot
2014-03-28Define Tactics.bring_hyps in the new monad.Pierre-Marie Pédrot
2014-03-27Removing tactic compatibility layer from Eqdecide.Pierre-Marie Pédrot
2014-03-27Cosmetic changes in Equality.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Removing tactic compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Inv.Pierre-Marie Pédrot
2014-03-26Removing tactic compatibility layer from Inv.Pierre-Marie Pédrot
2014-03-26STM: when an error occurs in a worker send back a bunch of statesEnrico Tassi
2014-03-26CoqIDE: better error reporting for Qed on incomplete proofEnrico Tassi
2014-03-26test for apply + TC resolutionEnrico Tassi
2014-03-26Adding an interface to Eqdecide and putting the grammar rules in a dedicatedPierre-Marie Pédrot
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-24Revert "Makefile: the initial build of grammar.cma is now directory-driven"Pierre Letouzey
2014-03-20Missing equalities in Names-like structures.Pierre-Marie Pédrot
2014-03-20Slightly more efficient Array.smartmap & related.Pierre-Marie Pédrot
2014-03-20Documenting the Print Strategy command.Pierre-Marie Pédrot
2014-03-19Adding a Print Strategy vernacular command. It allows to check thePierre-Marie Pédrot
2014-03-19Using non-normalized goals in tactic interpretation.Pierre-Marie Pédrot
2014-03-19Adding phantom types to discriminate normalized goals, and adding a way toPierre-Marie Pédrot
2014-03-18Remove the -fno-defer-pop cflagJason Gross
2014-03-18Printing backtraces in coqchk while in debug mode.Pierre-Marie Pédrot
2014-03-18Fixing checker with respect to new kernel name structure and hashmaps.Pierre-Marie Pédrot
2014-03-18STM: make the slave start from the most recent known stateEnrico Tassi
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-17Evarconv: exact_ise_stack looks to stack head before bodies or branchesPierre Boutillier
2014-03-17Fix test-suite 2255.vPierre Boutillier
2014-03-16consider_remaining_unif_problems respects Conv_oraclePierre Boutillier
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-03-13nanoPG: better copy/pasteEnrico Tassi
2014-03-13fix compilation with ocaml < 4Enrico Tassi
2014-03-13STM: perspective (tell the scheduler what the user sees)Enrico Tassi
2014-03-13Stateid: export a Set moduleEnrico Tassi
2014-03-13STM: move out a couple of submodulesEnrico Tassi
2014-03-12fake_ide: fix compilationEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 18:59:53 +0000