coq/doc/sphinx/language/extensions, branch master The formal proof system Extend Canonical Structure documentation. 2021-04-22T07:16:22+00:00 Jan-Oliver Kaiser 2020-05-15T09:44:29+00:00 9b35db9c7eb0cbc8e27c67f2ba2783fdd28ba247 This commit adds a more detailed explanation of what kinds of terms are allowed in fields of a canonical instance, how the fields are used as keys for canonical extension, what terms are considered overlapping, and how Coq reacts to overlapping fields. 
This commit adds a more detailed explanation of what kinds of terms are
allowed in fields of a canonical instance, how the fields are used as
keys for canonical extension, what terms are considered overlapping, and
how Coq reacts to overlapping fields.
Convert 2nd part of rewriting chapter to prodn 2021-03-08T19:48:20+00:00 Jim Fehrle 2020-09-13T03:54:22+00:00 0d33024ff79c38d52fde49e23d0e45d9c22eefbe 






Convert rewriting and proof-mode chapters to prodn
2020-12-30T19:48:37+00:00

Jim Fehrle

2020-09-13T03:54:22+00:00

e02120ed6580733db2276f0c11b4f432ea670ee3












typo
2020-12-04T10:10:03+00:00

Yves Bertot

2020-12-04T10:10:03+00:00

ffc0f5992e21a9dab5bead467cb41bbcc7face01












Fix #13283: improved error on `clear implicit` flag
2020-11-27T09:20:40+00:00

Fabian Kunze

2020-11-27T09:20:40+00:00

ce8569a3713536e510381e4d49d534a447cfe637












Adapting standard library, doc and test suite to ident->name renaming.
2020-11-22T12:28:40+00:00

Hugo Herbelin

2020-03-17T10:16:09+00:00

df8b5c7d83ad6e88af34d29bcc32c85bd42c2712












Review commit: improving the doc of boolean attributes.
2020-11-18T15:25:00+00:00

Théo Zimmermann

2020-11-14T17:44:57+00:00

ca42305f1ed1699065cffdef7d96bf5fcc0069be












[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.
2020-11-18T15:24:28+00:00

Emilio Jesus Gallego Arias

2020-11-12T19:21:36+00:00

c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b

We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).

We update the documentation, test-suite, and changelog.





We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).

We update the documentation, test-suite, and changelog.







Move destructuring let syntax closer to its documentation.
2020-11-14T12:40:45+00:00

Théo Zimmermann

2020-11-13T09:08:48+00:00

15183aafe292695c54ae234a1210c08c8e3cd378












[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.
2020-11-09T17:39:49+00:00

Théo Zimmermann

2020-11-09T17:39:49+00:00

a3869e5371c89629ddfd8ccdd1bdc0de12efe806

The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.





The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.