aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-04-04Prevent verbatim text from leaking out of comments. (See bug #2882)Guillaume Melquiond
2014-04-04Fixing coqchk. It was my fault, I misused canonical and user equalitiesPierre-Marie Pédrot
2014-04-04Fixing #3262 which revealed a non-progressing, hence looping,Hugo Herbelin
2014-04-04Support other forms of "Proof" in coqwc. (Fix for bug #2735)Guillaume Melquiond
2014-04-04Remove option -g as it is non-portable yet does not have any effect on the te...Guillaume Melquiond
2014-04-03Clean up the .merlinThomas Refis
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 18:25:18 +0000