aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-21[pp] Prepare for serialization, remove opaque glue.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove `Pp.stras`.Emilio Jesus Gallego Arias
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
2017-03-21[ide] ide_slave doesnt't need to capture stdoutEmilio Jesus Gallego Arias
2017-03-21[ide] Use "log via feedback".Emilio Jesus Gallego Arias
2017-03-21[safe-string] update dev/doc/changesEmilio Jesus Gallego Arias
2017-03-21Merge PR#134: Enable `-safe-string`Maxime Dénès
2017-03-21trivial: fix commentMatej Kosik
2017-03-20Merge PR#430: make `emit' tail recursiveMaxime Dénès
2017-03-20In the Kami project, that causes a stack overflow in one of the example filesPaul Steckler
2017-03-20[misc] Remove warnings about String.setEmilio Jesus Gallego Arias
2017-03-20Merge PR#479: [future] Remove unused parameter greedy.Maxime Dénès
2017-03-19Merge PR#487: Add a forgotten (?) line to "theories/Logic/vo.itarget".Maxime Dénès
2017-03-19Add a forgotten (?) line to "theories/Logic/vo.itarget".Matej Kosik
2017-03-17Merge PR#429: Don't require printing-only notation to be productiveMaxime Dénès
2017-03-17Merge PR#428: Report missing tactic arguments in error messageMaxime Dénès
2017-03-17Merge PR#437: Improve unification debug trace.Maxime Dénès
2017-03-17Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Maxime Dénès
2017-03-17Merge PR#442: Allow interactive editing of Coq.Init.LogicMaxime Dénès
2017-03-17Merge PR#451: Add η principles for sigma typesMaxime Dénès
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
2017-03-15Merge PR#267: Proposal for an update of the recommended style in programming ...Maxime Dénès
2017-03-14[safe-string] Enable -safe-string !Emilio Jesus Gallego Arias
2017-03-14[safe-string] toolsEmilio Jesus Gallego Arias
2017-03-14[safe-string] ideEmilio Jesus Gallego Arias
2017-03-14[safe-string] plugins/extractionEmilio Jesus Gallego Arias
2017-03-14[safe-string] ltac/profile_ltacEmilio Jesus Gallego Arias
2017-03-14[safe_string] toplevel/vernacEmilio Jesus Gallego Arias
2017-03-14[safe_string] toplevel/coqloopEmilio Jesus Gallego Arias
2017-03-14[safe-string] parsing/cLexerEmilio Jesus Gallego Arias
2017-03-14[safe_string] interp/dumpglobEmilio Jesus Gallego Arias
2017-03-14[safe_string] library/nameopsEmilio Jesus Gallego Arias
2017-03-14[safe_string] kernel/cemitcodesEmilio Jesus Gallego Arias
2017-03-14[toplevel] Remove unusable option -notopEmilio Jesus Gallego Arias
2017-03-14Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoMaxime Dénès
2017-03-14Report missing tactic arguments in error messageTej Chajed
2017-03-14[safe-string] kernel/nativevaluesEmilio Jesus Gallego Arias
2017-03-14[safe_string] kernel/term_typingEmilio Jesus Gallego Arias
2017-03-14[safe-string] lib/miscelaneaEmilio Jesus Gallego Arias
2017-03-14[safe-string] lib/cUnixEmilio Jesus Gallego Arias
2017-03-14[safe_string] lib/cThreadEmilio Jesus Gallego Arias
2017-03-14Merge PR#438: Fix V7 syntax in refman.Maxime Dénès
2017-03-14Merge PR#412: Remove outdated comment from 2002.Maxime Dénès
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-03-14Merge PR#477: [travis] Basic support for overlays.Maxime Dénès
2017-03-14Merge PR#473: [ci] Document that sudo: false is slowerMaxime Dénès
2017-03-14Merge PR#464: [META] More fixesMaxime Dénès
2017-03-14Merge PR#465: Fix #5132: coq_makefile generates incorrect install goalMaxime Dénès
2017-03-14Fix #5132: coq_makefile generates incorrect install goalVadim Zaliva
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:42:35 +0000