aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-02-24Simplifying the proof of NoRetractToModalProposition.paradox inHugo Herbelin
2017-02-23Fixing #use"include" after vernac is added and ltac is moved to a plugin.Hugo Herbelin
2017-02-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-22Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2017-02-21[travis] track an 8.7 specific branch of HoTT.Maxime Dénès
2017-02-21Merge PR#309: Ltac as a pluginMaxime Dénès
2017-02-21Add empty ltac_plugin file for forward compatibility.Maxime Dénès
2017-02-20Merge PR#189: Remove tabulation support from pretty-printing.Maxime Dénès
2017-02-19Fixing debugger after the split of toplevel into vernac.Pierre-Marie Pédrot
2017-02-17remove obsolete file dev/Makefile.ougPierre Letouzey
2017-02-17Removing spurious folder includes in coq_makefile.Pierre-Marie Pédrot
2017-02-17Documenting the pluginification of Ltac.Pierre-Marie Pédrot
2017-02-17Fix .gitignore.Pierre-Marie Pédrot
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2017-02-16Fixing #5339 (anomaly with 'pat in record parameters).Hugo Herbelin
2017-02-16Merge PR#403: Split Vernacular Processing from ToplevelMaxime Dénès
2017-02-16Merge PR#431Maxime Dénès
2017-02-15[travis] [External CI] CompCert official 8.6 support + UniMathEmilio Jesus Gallego Arias
2017-02-15[travis] [External CI] Factor out math-comp installs.Emilio Jesus Gallego Arias
2017-02-15Make Obligations see fix_exnEnrico Tassi
2017-02-15[stm] Remove unused legacy stm interface.Emilio Jesus Gallego Arias
2017-02-15[cosmetic] Reorder makefile as suggested by @herbelinEmilio Jesus Gallego Arias
2017-02-15[stm] Reenable Show Script command.Emilio Jesus Gallego Arias
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2017-02-15Merge PR#314: Miscellaneous fixes for Ocaml warnings.Maxime Dénès
2017-02-15[unicode] Address comments in PR#314.Emilio Jesus Gallego Arias
2017-02-14[safe-string] Switch to buffer to `Bytes`Emilio Jesus Gallego Arias
2017-02-14[safe-string] Use `String.init` to build string.Emilio Jesus Gallego Arias
2017-02-14[misc] Remove unused binding.Emilio Jesus Gallego Arias
2017-02-14Merge PR#253: Sort Search results by relevanceMaxime Dénès
2017-02-14Test-suite: output of SearchArnaud Spiwack
2017-02-13Merge PR#349: Proofview: tclINDEPENDENTLMaxime Dénès
2017-02-10Proofview: tclINDEPENDENTLEnrico Tassi
2017-02-09Turning an anomaly on 'pat into a proper "unsupported" error message.Hugo Herbelin
2017-02-09Fixing bug #5346 (an unimplemented application of 'pat).Hugo Herbelin
2017-02-08Merge PR#405: Type cleanup in `Metasyntax`Maxime Dénès
2017-02-08Merge PR#393: Replace Typeops with Fast_typeopsMaxime Dénès
2017-02-07Revert "Extraction: avoid deprecated functions of module String"Pierre Letouzey
2017-02-07Extraction cosmetic: no whitespaces in printing empty modulesPierre Letouzey
2017-02-07Extraction: remove the "print to devnull" hack now that pp isn't lazy anymorePierre Letouzey
2017-02-07Extraction: avoid deprecated functions of module StringPierre Letouzey
2017-02-07Extraction: simplify the generated code for difficult name conflictsPierre Letouzey
2017-02-07Extraction : get_duplicates (via option) instead of check_duplicates (via Not...Pierre Letouzey
2017-02-07configure: avoid deprecated warningsPierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-02-07Merge PR#425: [travis] [External CI] [geocoq] don't build slow fileMaxime Dénès
2017-02-07[travis] [External CI] [geocoq] don't build slow fileEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 09:41:57 +0000