aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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
2018-05-05More fixes in the Generalized Rewriting chapter.Théo Zimmermann
2018-05-05[sphinx] Replace remaining `@natural` by `@num`.Théo Zimmermann
2018-05-05[sphinx] More use of cmd references in Extraction chapter.Théo Zimmermann
2018-05-05[sphinx] Use references for command Info.Théo Zimmermann
2018-05-05[sphinx] More reference fixes.Théo Zimmermann
2018-05-05[sphinx] Fix a porting mistake.Théo Zimmermann
2018-05-05[sphinx] Use references for Print.Théo Zimmermann
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
2018-05-05Add direct reference to congruence with.Théo Zimmermann
2018-05-05Clean-up around options.Théo Zimmermann
2018-05-05debug trivial and debug auto were not in the tactic index.Théo Zimmermann
2018-05-05Fix failing example in refman.Théo Zimmermann
2018-05-05[sphinx] Fix some references.Théo Zimmermann
2018-05-05[sphinx] Use option direct reference.Théo Zimmermann
2018-05-05[sphinx] Fix a typo that appeared during the migration.Théo Zimmermann
2018-05-05[sphinx] Fix a hardcoded reference.Théo Zimmermann
2018-05-05[sphinx] Backport reformulation.Théo Zimmermann
2018-05-05[sphinx] Backport fix of typo.Théo Zimmermann
2018-05-05Fix typo in Coercions chapter.Théo Zimmermann
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7416: Fix #7415. Printing Width was not applied to error messages.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Pierre-Marie Pédrot
2018-05-04Fix #7413: coqdep warning on repeated filesGaëtan Gilbert
2018-05-03Merge PR #7134: When an error comes from loading the prelude, tell it happene...Emilio Jesus Gallego Arias
2018-05-03Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_substPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:22:34 +0000