aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-03-12Stm: smarter delegation policyEnrico Tassi
2014-03-12CoqIDE: Errors page gets red if not emptyEnrico Tassi
2014-03-12CoqIDE: detachable message/error/jobs panesEnrico Tassi
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-11Fix (3243): univ constraints of module subtyping were not propagatedEnrico Tassi
2014-03-10Useless Array.to_list in Typeops.Pierre-Marie Pédrot
2014-03-10Evarconv unification respects Conv_oraclePierre Boutillier
2014-03-10MaybeFlexible semantic changesPierre Boutillier
2014-03-10Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Guillaume Melquiond
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2014-03-08Also use HMaps in KNmap.Pierre-Marie Pédrot
2014-03-07Potentially unused computation in Goal.Pierre-Marie Pédrot
2014-03-07Useless tactic bindings in Tacticals.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 23:59:38 +0000