aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2018-03-13[Sphinx] Comment out metadata for unused backendsMaxime Dénès
2018-03-13[Sphinx] Remove information for .chm backendMaxime Dénès
2018-03-13[Sphinx] add bibliographyMaxime Dénès
2018-03-13[Sphinx] Add indexesMaxime Dénès
2018-03-12[Sphinx] Add table of contentsMaxime Dénès
2018-03-12[Sphinx] Add doc preambleMaxime Dénès
2018-03-12[Sphinx] Add a few grammar constructionsMaxime Dénès
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Documentation for Cumulativity Weak Constraints.Gaëtan Gilbert
2018-03-09Merge PR #6480: Allow Prop as source for coercionsMaxime Dénès
2018-03-09Merge PR #6818: Sphinx doc infrastructureMaxime Dénès
2018-03-09Moving Gitlab CI documentation build to the main Coq build.Maxime Dénès
2018-03-09Integration of a sphinx-based documentation generator.Maxime Dénès
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-09doc and changes for coercion from prop/typecharguer
2018-03-09Merge PR #6937: Add empty compat file for Coq 8.8Maxime Dénès
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-08Merge PR #6903: [compat] Remove "Shrink Abstract"Maxime Dénès
2018-03-07Add empty compat file for Coq 8.8Jason Gross
2018-03-06Remove outdated information regarding the FAQ.Théo Zimmermann
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-05Deprecate Focus and Unfocus.Théo Zimmermann
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #915: Fix rewrite in * side conditionsMaxime Dénès
2018-03-04Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...Maxime Dénès
2018-03-04Fix typos.Théo Zimmermann
2018-03-03[compat] Remove "Intuition Iff Unfolding"Emilio Jesus Gallego Arias
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
2018-02-28Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Hugo Herbelin
2018-02-28[toplevel] [vernac] Remove Load hack and check supported scenarios.Emilio Jesus Gallego Arias
2018-02-27Typo in the documentation of the `pattern` tacticJoachim Breitner
2018-02-24Merge PR #6819: Document Arguments extra scopes flagMaxime Dénès
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-22Document Arguments extra scopes flagJasper Hugunin
2018-02-20Doc: add Decimal-related files to index-list.html.templateJason Gross
2018-02-20Documenting use of primitive entry names for restricting syntax in notations.Hugo Herbelin
2018-02-20Extended documentation for notations referring to binders.Hugo Herbelin
2018-02-20A first step at refreshing and documenting the new feature.Hugo Herbelin
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance informa...Maxime Dénès
2018-02-11Documentation for cumulative inductive variance.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 02:21:23 +0000