aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-13Document instantiate (ident := term) and make it the preferred variant.Théo Zimmermann
2017-06-13Document Show ident.Théo Zimmermann
2017-06-13Document evar naming syntax.Théo Zimmermann
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-12[proof] Move bullets to their own module.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-24 22:25:59 +0000