aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-13[travis] overlay + extra deps for math-classes (and formal-topology)Pierre Letouzey
2017-06-13Merge PR#757: Better sectioning on travis log printing in test-suiteMaxime Dénès
2017-06-13Documenting the change of default flag value of Refine.refine.Pierre-Marie Pédrot
2017-06-13Turn the default behaviour of the refine primitive into the safe one.Pierre-Marie Pédrot
2017-06-13Explicit the unsafe flag of all calls to Refine.refine.Pierre-Marie Pédrot
2017-06-13[travis] adapt CoLoR compilation to depend on the bignum packagePierre Letouzey
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2017-06-13Merge PR#743: Update .gitignoreMaxime Dénès
2017-06-13Merge PR#764: Point ci-hott at a newer version of HoTTMaxime Dénès
2017-06-13Merge PR#772: Store plugins/micromega/micromega.{ml,mli} files in the reposit...Maxime Dénès
2017-06-12Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ge...Matej Košík
2017-06-12Merge PR#715: Add coq-dpdgraph ciMaxime Dénès
2017-06-12[travis overlay] Partially Revert 013c0232953f1f58Jason Gross
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-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-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-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-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-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-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