aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-01-19Using full paths in coqdep -dumpgraph.Pierre-Marie Pédrot
2014-01-19Fixing coqdep graph printing. The transitive reduction algorithm was bugged.Pierre-Marie Pédrot
2014-01-19Adding a default object to generic argument registering mechanism.Pierre-Marie Pédrot
2014-01-19Fixing an interpretation bug with tactics in notations. For some obscurePierre-Marie Pédrot
2014-01-19Fixing checker compilation, which was broken by the following commit:Pierre-Marie Pédrot
2014-01-18Relaxing the sort elimination check to allow for let-bindings in arities.Maxime Dénès
2014-01-18Makefiles use $(foo), not $foo, for variablesJason Gross
2014-01-18Fixup make clean and .merlinPierre Boutillier
2014-01-17Follow-up of bugfix for #3204: local definitions were not handled properly.Pierre-Marie Pédrot
2014-01-17Fixing bug #1758: Print Hint output can be misleading if variable shadows hyp...Pierre-Marie Pédrot
2014-01-17Update .mailmap with recent contributors.Arnaud Spiwack
2014-01-16Fixing bugs #1039: Hypotheses don't respect Barendregt conventionPierre-Marie Pédrot
2014-01-16Implementing transitive reduction in the dependency graph printingPierre-Marie Pédrot
2014-01-15Christmas is over...Maxime Dénès
2014-01-15Test case containing a proof of false due to a DeBruijn off-by-one error in theMaxime Dénès
2014-01-14-schedule-vi-checking generates better scriptEnrico Tassi
2014-01-14STM: fix -async-proofs lazyEnrico Tassi
2014-01-14Removing unused tactics in rewrite.Pierre-Marie Pédrot
2014-01-13Make Require verbosePierre Boutillier
2014-01-13rename Paral-ITP demo fileEnrico Tassi
2014-01-13Paral-ITP demo: better commentsEnrico Tassi
2014-01-13STM: fix very simple demoEnrico Tassi
2014-01-13Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Pierre Boutillier
2014-01-13Fixing typo in reference manual from previous commitHugo Herbelin
2014-01-13Documenting old but useful command "Print Tables".Hugo Herbelin
2014-01-11'Pretty' printer for wf_pathsPierre
2014-01-10Fixing bug #3144.Pierre-Marie Pédrot
2014-01-10Useless Array.of_listPierre-Marie Pédrot
2014-01-10Omega: avoiding distinct proof-terms on repeated identical runsPierre Letouzey
2014-01-10Exporting the full pretyper options in Goal.constr_of_raw.Pierre-Marie Pédrot
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
2014-01-09Goodbye typerex, Hello merlinPierre
2014-01-09md5 for MacOSPierre
2014-01-08Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evdPierre Letouzey
2014-01-07typosEnrico Tassi
2014-01-07STM: additional fix for STM + vm_computeEnrico Tassi
2014-01-06Adding a -dumpgraph option to Coqdep that output the graph dependency of thePierre-Marie Pédrot
2014-01-06CoqIDE: do not unfocus if not needed on errors (closes: 3197)Enrico Tassi
2014-01-06fix simple test for paral-itpEnrico Tassi
2014-01-06fix typoEnrico Tassi
2014-01-06STM: handle side effects of workers correctlyEnrico Tassi
2014-01-06STM: fix worker crash when doing vm_computeEnrico Tassi
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2014-01-06Add a test suite file for Ltac's "+" tactical.Arnaud Spiwack
2014-01-06Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...Arnaud Spiwack
2014-01-05refman: fist stab at Asynchronous ProofsEnrico Tassi
2014-01-05STM: modules do not prevent proofs from being ASyncEnrico Tassi
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2014-01-05Fix coqc -time (Closes: 3201)Enrico Tassi
2014-01-05nanoPG: compete rewriting with more Emacs/PG like featuresEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 02:02:58 +0000