aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-05-09A few fixes in chapter tactics.Hugo Herbelin
2018-05-08Merge PR #7459: Try to fix CODEOWNERSThéo Zimmermann
2018-05-08Don't use ref universe_opt_substGaëtan Gilbert
2018-05-08Merge PR #7446: [lib] Re-add `set_timeout` to help users workaround #7408Pierre-Marie Pédrot
2018-05-08intermediary stage with an EConstr containing a hand-made evar, fautyYves Bertot
2018-05-08corrects a problem in documenting how to run the demoYves Bertot
2018-05-08problems with bullet listsYves Bertot
2018-05-08try with triple backticksYves Bertot
2018-05-08attempt to make code inclusions appear correctlyYves Bertot
2018-05-08Try to fix CODEOWNERSMaxime Dénès
2018-05-08[gitlab] Do expensive builds with a flambda-compiled Coq.Emilio Jesus Gallego Arias
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-05-08[CoqProject] Add some comments and remove unnecessary use of Pp.Emilio Jesus Gallego Arias
2018-05-08[coqdep] Remove unnecessary dependency on Pp and CError.Emilio Jesus Gallego Arias
2018-05-08[coqdep] Minor cleanups.Emilio Jesus Gallego Arias
2018-05-08[toplevel] Don't ignore output filename provided by user in -oEmilio Jesus Gallego Arias
2018-05-07Merge branch 'master' of https://github.com/ybertot/plugin_tutorialsYves Bertot
2018-05-07adds a copy of the show_proof commandYves Bertot
2018-05-07[gitlab] Add bleeding-edge flambda build.Emilio Jesus Gallego Arias
2018-05-07[lib] Re-add `set_timeout` to help users workaround #7408Emilio Jesus Gallego Arias
2018-05-07[vernac] taint two out-of-api `to_constr` use in `comDefinition`.Emilio Jesus Gallego Arias
2018-05-07Merge pull request #1 from matejkosik/masterYves Bertot
2018-05-07Add CODEOWNERS entry for check-owners*.shGaëtan Gilbert
2018-05-07Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging)Maxime Dénès
2018-05-07Merge PR #7371: Propose some updates of the CODEOWNER file.Maxime Dénès
2018-05-07Merge PR #7445: [ci] Add ounit to the base Docker package set.Gaëtan Gilbert
2018-05-07Merge PR #7301: [sphinx] Backport forgotten updates during the migration & ot...Maxime Dénès
2018-05-07Merge PR #7440: [ci] Add a default target to `Makefile.ci`Gaëtan Gilbert
2018-05-07fix some detailsMatej Košík
2018-05-07[ci] Add ounit to the base Docker package set.Emilio Jesus Gallego Arias
2018-05-07Merge PR #7427: Fix #7413: coqdep warning on repeated filesPierre-Marie Pédrot
2018-05-07fix some detailsMatej Košík
2018-05-07add some more material (preliminary provided in "tuto2" directory)Matej Košík
2018-05-06Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CIGaëtan Gilbert
2018-05-06Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow kern...Maxime Dénès
2018-05-06[ci] Add a default target to `Makefile.ci`Emilio Jesus Gallego Arias
2018-05-05[gitlab] [circleci] Use a Custom Docker Image as base CI setup.Emilio Jesus Gallego Arias
2018-05-05[sphinx] Fixes around apply, including indentation and fixing a Coq warning.Théo Zimmermann
2018-05-05[sphinx] Fixes around refine, including indentation and a hard-coded ref.Théo Zimmermann
2018-05-05[sphinx] Improve typeclass chapter.Théo Zimmermann
2018-05-05[sphinx] Add indices for only, all and par.Théo Zimmermann
2018-05-05[sphinx] Improvements around injection tactic.Théo Zimmermann
2018-05-05[sphinx] Improve part about Hints.Théo Zimmermann
2018-05-05[sphinx] Re-indent to get much better rendering.Théo Zimmermann
2018-05-05Remove duplicate Introduction title.Théo Zimmermann
2018-05-05[sphinx] Backport changes from #5979.Théo Zimmermann
2018-05-05Two more uses of verbatim in doc.Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
2018-05-05Remove duplicate Extraction commands documentation.Théo Zimmermann
2018-05-05Add some refs in the Omega chapter.Théo Zimmermann