aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-12Merge PR#709: Bytecode compilation apart from 'make world', againMaxime Dénès
2017-06-12Merge PR#718: API cleanup: aliasesMaxime Dénès
2017-06-12Temporary overlay, waiting for upstream PR merges.Maxime Dénès
2017-06-12Merge PR#707: add support for "-bypass-API" argument to "coq_makefile"Maxime Dénès
2017-06-12add overlaysMatej Košík
2017-06-12Add support for "-bypass-API" argument of "coq_makefile"Matej Košík
2017-06-12make test-suite/save-logs.sh usable also on old MacOS XMaxime Denes
2017-06-12zify: force reduction of (Z.max 0 0) and similar (fix #5439)Pierre Letouzey
2017-06-12zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)Pierre Letouzey
2017-06-12[lib] Remove obsolete state-management function add_frozen_stateEmilio Jesus Gallego Arias
2017-06-12Remove commented documentation for Show Tree.Théo Zimmermann
2017-06-12Fix ocamldebug for the APIGaëtan Gilbert
2017-06-12Remove Show Thesis command which was never implemented.Théo Zimmermann
2017-06-12Remove non-working Show Tree and Show Node commands.Théo Zimmermann
2017-06-12Remove more dead code (follow-up of previous commit).Théo Zimmermann
2017-06-12Remove Show Implicit Arguments command.Théo Zimmermann
2017-06-12Remove Show Goal "uid" command.Théo Zimmermann
2017-06-11Point ci-hott at a newer version of HoTTJason Gross
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-11A stronger test that #use"include";; works well.Hugo Herbelin
2017-06-11Fixing base_include after loc is an option (30d3515).Hugo Herbelin
2017-06-11Normalize deprecation notices of ./configureThéo Zimmermann
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-10Fix Travis sectioningJason Gross
2017-06-10don't leak unqualified identifiers from the macroMatej Košík
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-10[toplevel] Print error header on fatal batch error.Emilio Jesus Gallego Arias
2017-06-09Better sectioning on travis log printing in test-suiteJason Gross
2017-06-09Fix Bug #5568, no dup notation warnings on repeated module importsPaul Steckler
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-09Makefile.common: remove an obsolete comment after PR#499Pierre Letouzey
2017-06-08Mirror dpdgraph's travis test more accuratelyJason Gross
2017-06-08Remove coq-dpdgraph overlayJason Gross
2017-06-08Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Théo Zimmermann
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Adding a test case as requested in bug 5205.Théo Zimmermann
2017-06-08Remove overlay.Maxime Dénès
2017-06-08Merge PR#652: Put all plugins behind an "API".Maxime Dénès
2017-06-07Update .gitignoreJason Gross
2017-06-07[stm] More fixes for nested commands [bugzilla 5589]Emilio Jesus Gallego Arias
2017-06-07Fix documentation of Typeclasses eauto :=Théo Zimmermann
2017-06-07completing a sentence in a commentMatej Košík
2017-06-07[kernel] Improve proof using message, fixes bugzilla #3613Emilio Jesus Gallego Arias
2017-06-07add overlaysMatej Košík
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-07Merge PR#698: Trunk miscMaxime Dénès
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-07Merge PR#669: Ssr mergeMaxime Dénès
2017-06-06Overlay.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 20:19:25 +0000