aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2018-03-26Move Classes.tex to type-classes.rstMatthieu Sozeau
2018-03-22Merge branch 'master' into sphinx-doc-chapter-22Guillaume Melquiond
2018-03-22Merge branch 'master' into sphinx-doc-chapter-21Guillaume Melquiond
2018-03-22Merge branch 'master' into sphinx-doc-chapter-19Guillaume Melquiond
2018-03-22[Sphinx] Move chapter 22 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 21 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 19 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 17 to new infrastructureMaxime Dénès
2018-03-16[Sphinx] Add chapter 11Maxime Dénès
2018-03-15[Sphinx] Move chapter 3 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 16 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 14 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 13 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 12 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 10 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 8 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 5 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 4 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 2 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move credits to new infrastructureMaxime Dénès
2018-03-13[Sphinx] Move introduction to new infrastructureMaxime 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 #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-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-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 #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-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-22Document Arguments extra scopes flagJasper Hugunin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 08:03:21 +0000