coq - The formal proof system

Age	Commit message (Expand)	Author
2020-05-01	Create section on basics with just flags, options and tables.	Théo Zimmermann
2020-05-01	Create section on basics with just lexical conventions and attributes.	Théo Zimmermann
2020-05-01	Extract lexical conventions and attributes from Gallina chapter.	Théo Zimmermann
2020-04-26	Convert syntax extensions chapter to prodn	Jim Fehrle
2020-04-13	Update syntax of Import / Export in documentation.	Théo Zimmermann
2020-04-13	doc for partial imports	Gaëtan Gilbert
2020-04-11	Merge PR #11961: Convert vernac commands chapter to prodn, update syntax	Théo Zimmermann
2020-04-10	Convert vernac commands chapter to prodn, update syntax	Jim Fehrle
2020-04-07	Support universe bindings and universe constraints in Let definitions.	Théo Zimmermann
2020-04-03	Split four sections out of the Gallina extensions chapter.	Théo Zimmermann
2020-04-03	Move section in records in appropriate location (inside core).	Théo Zimmermann
2020-04-03	Move section on sections in appropriate location (inside core).	Théo Zimmermann
2020-04-03	Move section on funind in appropriate location (inside libraries).	Théo Zimmermann
2020-04-03	Move section on implicit arguments in appropriate location (inside extensions).	Théo Zimmermann
2020-04-03	Extract section on implicit arguments from Gallina extensions.	Théo Zimmermann
2020-04-03	Extract section on funind from Gallina extensions.	Théo Zimmermann
2020-04-03	Remove sections on records, sections, funind and implicit arguments from gall...	Théo Zimmermann
2020-04-03	Extract section on sections from Gallina extensions.	Théo Zimmermann
2020-04-03	Extract section on records from Gallina extensions.	Théo Zimmermann
2020-03-29	Merge PR #11859: Warn when non exactly parsing non floating-point	Hugo Herbelin
2020-03-26	Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.	Théo Zimmermann
2020-03-26	Removing deprecated destruct syntax _eqn.	Hugo Herbelin
2020-03-26	Shrink refman-prelude files.	Théo Zimmermann
2020-03-26	Remove outdated mention of -allow-sprop.	Théo Zimmermann
2020-03-26	Print a warning when parsing non floating-point values.	Pierre Roux
2020-03-25	Doc_grammar: Update cmd:: and tacn:: constructs in .rsts	Jim Fehrle
2020-03-25	Convert Gallina Extensions to use prodn	Jim Fehrle
2020-03-20	Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.	Pierre-Marie Pédrot
2020-03-19	Document all the existing attributes.	Théo Zimmermann
2020-03-19	Adapt to sub-TOC not showing in PDF output.	Théo Zimmermann
2020-03-19	[refman] Move chapters into new structure.	Théo Zimmermann
2020-03-09	Remove some productionlists	Jim Fehrle
2020-03-04	Adding support for an "only parsing" modifier in "where"-based notations.	Hugo Herbelin
2020-02-29	Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.	Clément Pit-Claudel
2020-02-28	Convert Gallina Vernac to use prodn	Jim Fehrle
2020-02-27	Fix #11696: link from refman to stdlib doc is dead.	Théo Zimmermann
2020-02-21	Merge PR #11261: Use implicit types for printing (granting wish #10366).	Emilio Jesus Gallego Arias
2020-02-18	Updating reference manual and adding a change log entry.	Hugo Herbelin
2020-02-17	New syntax [Inductive Acc A R \| x : Prop := ...]	Gaëtan Gilbert
2020-02-17	Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"	Gaëtan Gilbert
2020-02-14	Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Para...	Maxime Dénès
2020-02-13	Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)	Gaëtan Gilbert
2020-02-13	Arguments: removing the restriction to set an anonymous parameter implicit.	Hugo Herbelin
2020-02-11	Document the ability to use manual implicit arguments in subexpressions.	Hugo Herbelin
2020-02-04	Apply suggestions from Hugo	SimonBoulier
2020-02-04	Update doc for non max implicit arguments	SimonBoulier
2020-01-19	Merge PR #11368: Turn trailing implicit warning into an error	Hugo Herbelin
2020-01-09	Merge PR #11164: [CS] allow Let variable to be canonical	Pierre-Marie Pédrot
2020-01-08	Trailing implicit: Maxime's suggestions	SimonBoulier
2020-01-07	Merge PR #11369: [refman] Correct manual about implicit parameters in inductives	Théo Zimmermann