coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-01-07	Correct manual about implicit parameters in inductives.	SimonBoulier

2020-01-07	Trailing implicit error: documentation	SimonBoulier

2020-01-06	doc: mention limitation of bidi hints vs program	Gaëtan Gilbert
	No example as I'm not familiar enough with Program to make one.
2020-01-06	Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx ↵	Clément Pit-Claudel
	migration. Reviewed-by: jfehrle
2019-12-31	Merge PR #11325: [refman] Add missing s.	Pierre-Marie Pédrot
	Reviewed-by: jfehrle
2019-12-29	Remove :flag: that appears in the output	Jim Fehrle

2019-12-29	[refman] Fix bad quoting practice leftover from Sphinx migration.	Théo Zimmermann

2019-12-29	Merge PR #11314: Convert productionlists in the Gallina chapter up to the ↵	Théo Zimmermann
	Vernacular section to prodns Reviewed-by: Zimmi48
2019-12-28	Convert productionlists to prodns	Jim Fehrle

2019-12-28	Update doc/sphinx/language/gallina-extensions.rst	Kazuhiko Sakaguchi
	Co-Authored-By: Cyril Cohen <CohenCyril@users.noreply.github.com>
2019-12-28	Extend `Print Canonical Projections` with a search functionality	Kazuhiko Sakaguchi
	The `Print Canonical Projections` command now can take constants and prints only the unification rules that involves or are synthesized from given constants.
2019-12-24	[Attributes] accept #[canonical] (Let\|Definition)	Enrico Tassi

2019-12-22	[refman] Add missing s.	Théo Zimmermann

2019-12-02	[CS] support #[local] attribute	Enrico Tassi

2019-11-20	Update grammar in the Terms section of Gallina chapter	Jim Fehrle
	Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-11-14	Fix doc for universes(foo) attributes	Gaëtan Gilbert
	Fix #10570
2019-11-08	Merge PR #11050: Replace "option" in doc when it refers to a flag	Théo Zimmermann
	Reviewed-by: Zimmi48
2019-11-06	Replace "option" in doc when it refers to a flag	Jim Fehrle

2019-11-04	Cite POPL19 SProp paper	Gaëtan Gilbert
	Close #10242
2019-11-01	docs(gallina-extensions.rst): Say more on float literals extraction	Erik Martin-Dorel

2019-11-01	docs: Add refman+stdlib documentation	Erik Martin-Dorel

2019-10-31	Merge PR #10985: Print argument info as an Arguments command in About	Emilio Jesus Gallego Arias
	Ack-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: ejgallego
2019-10-31	Merge PR #10997: Implement the unsupported attribute error using the warning ↵	Emilio Jesus Gallego Arias
	system Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-10-31	Doc: index command Arguments with assert	Gaëtan Gilbert

2019-10-30	Implement the unsupported attribute error using the warning system	Gaëtan Gilbert
	This means we can disable it to ignore unsupported attributes. For instance this would be useful if we change some behaviour of `Cmd` and add an attribute `att` to restore the old behaviour, then `#[att] Cmd` is backwards compatible if the warning is disabled.
2019-10-30	Use bullets and indentation (but the result rendering is weird).	Théo Zimmermann

2019-10-30	Use explicit match as suggested by Clément.	Théo Zimmermann

2019-10-30	[refman] Add a second example of contradiction when positivity checking is ↵	Théo Zimmermann
	disabled.
2019-10-30	[refman] Give an example of contradiction when positivity checking is disabled.	Théo Zimmermann

2019-10-22	documentation fixes	Antonio Nikishaev
	document « Property » more documentation fixes [doc] destructed → destructured [doc] another le_minus→lt_1_r [doc] @jfehrle suggestions [doc] more minor fixes
2019-10-06	Fix #10831: minor issues in documentation of Function.	Théo Zimmermann

2019-08-26	Document `Template Check` flag and add changelog entry for 9918	Matthieu Sozeau
	Fix changelog entry Fix build of the user manual Markup fixes from Théo Zimmermann Update doc and changelog and improve error messages.
2019-08-16	Add documentation for typing flags.	SimonBoulier

2019-08-05	Remove reference to removed option Printing Primitive Projection Compatibility	Jim Fehrle

2019-07-30	Merge PR #10430: [Extraction] Add support for primitive integers	Maxime Dénès
	Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-28	Update documentation on tokens, use "int" and "num"	Jim Fehrle
	for integers and natural nums
2019-07-22	[Int63] Implement all primitives in OCaml	Vincent Laporte
	Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are implemented in the kernel so that they can be used by OCaml code (e.g., extracted code) as the other primitives.
2019-07-22	[Extraction] Add support for primitive integers	Vincent Laporte
	The ExtrOCamlInt63 module can be required to map primitives from the Int63 module to their OCaml implementation (module Uint63 from the kernel).
2019-06-06	`deprecated` attribute support for notations and syntactic definitions	Maxime Dénès
	We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter.
2019-06-04	[function] always open a proof when used with `wf` or `measure`	Enrico Tassi

2019-05-28	[elaboration] Bidirectionality hints	Maxime Dénès
	This feature makes it possible to tell type inference to type applications of a global `foo` using typing information from the context once the `n` first arguments are known. The syntax is: `Arguments foo x y \| z`. Closes #7910
2019-05-24	Merge PR #10167: do not parse `\|` as infix in patterns; parse `\|}` as `\|` `}`	Emilio Jesus Gallego Arias
	Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ggonthier Reviewed-by: herbelin Ack-by: jfehrle Reviewed-by: mattam82
2019-05-23	do not parse `\|` as infix in patterns; parse `\|}` as `\|` `}`	Georges Gonthier
	* use mixfix `(p1 \| … \| pn)` notation for nested disjunctive patterns, rather than infix `\|`, making pattern syntax consistent with term syntax. * disable extending `pattern` grammar with notation incompatible with the nested disjunctive pattern syntax `(p1 \| … \| pn)`, such as the `(p \| q)` divisibility notation used by `Numbers`. * emit a (disabled by default) `disj-pattern-notation` warning when such `Notation` is attempted. * update documentation accordingly; document incompatibilities in `changelog`. * comment special treatment of `(num)` in grammar. * update file extensions in `Pcoq` header comment. * correct the keyword declarations to reflect the contents of the grammar files; perhaps there should be an option to disable implicit keyword extension in a `.mlg` file, so that these lists could actually be checked. * parse the `\|}` manifest record terminator as `\|` followed by `}`, eliminating the `\|}` token which conflicts with notations that use `\|` as a terminator (such as, absolute value, norm, or cardinal in MathComp). Since `\|` is now an `operconstr` _and_ `pattern` terminator, `bar_cbrace` rule checks for contiguous symbols, this change entails no visible behaviour change.
2019-05-23	Define many undefined tokens, and other misc fixes.	Théo Zimmermann
	Progress towards #9411, extracted from #10118, rebased ontop of #10192.
2019-05-22	[refman] Give explicit names to the various 'Arguments' commands	Clément Pit-Claudel

2019-05-22	Merge PR #10178: Improve doc for generalizing binders	Théo Zimmermann
	Reviewed-by: Zimmi48
2019-05-22	Improve doc for generalizing binders	Gaëtan Gilbert

2019-05-19	[refman] Fix up the grammar entry for field_def	Clément Pit-Claudel

2019-05-19	[refman] Misc fixes (indentation, whitespace, notation syntax)	Clément Pit-Claudel

2019-05-19	Merge PR #10143: Add dedicated syntax for alternatives (abc \| def) in manual ↵	Théo Zimmermann
	notations Reviewed-by: Zimmi48 Ack-by: jfehrle