coq - The formal proof system

Age	Commit message (Expand)	Author
2018-02-21	Remove from CircleCI builds that are already taken care of by Travis.	Théo Zimmermann
2018-02-21	Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`	Maxime Dénès
2018-02-21	Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred	Maxime Dénès
2018-02-21	Merge PR #6767: [ci] add elpi	Maxime Dénès
2018-02-21	Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)	Maxime Dénès
2018-02-21	Merge PR #6283: A pre-commit hook to magically fix whitespace issues.	Maxime Dénès
2018-02-21	Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...	Maxime Dénès
2018-02-21	Merge PR #6740: Adding a sanity check on inductive variance subtyping.	Maxime Dénès
2018-02-21	Update CREDITS.	Théo Zimmermann
2018-02-21	More accurate and complete headers.	Théo Zimmermann
2018-02-21	Mention the CREDITS file in CONTRIBUTING.	Théo Zimmermann
2018-02-21	Remove redundant COPYRIGHT file.	Théo Zimmermann
2018-02-21	coqdev.el: add space at the end of compile-command	Gaëtan Gilbert
2018-02-20	Add CHANGES entry for decimals in prelude	Jason Gross
2018-02-20	Update SearchPattern.out for numeral notations	Jason Gross
2018-02-20	Doc: add Decimal-related files to index-list.html.template	Jason Gross
2018-02-20	Decimal goodies : conversion to/from Coq strings	Pierre Letouzey
2018-02-20	Decimal: proofs that conversions from/to nat,N,Z are bijections	Pierre Letouzey
2018-02-20	Decimal: simple representation of base-10 numbers	Pierre Letouzey
2018-02-20	Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Hugo Herbelin
2018-02-20	overlay for ltac2 and Equations	Enrico Tassi
2018-02-20	proofview: goals come with a state	Enrico Tassi
2018-02-20	Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).	Hugo Herbelin
2018-02-20	Adding a test for wish #5532.	Hugo Herbelin
2018-02-20	Documenting use of primitive entry names for restricting syntax in notations.	Hugo Herbelin
2018-02-20	Extended documentation for notations referring to binders.	Hugo Herbelin
2018-02-20	Trying a hack to support {'pat\|P} without breaking compatibility.	Hugo Herbelin
2018-02-20	Adding notations of the form "{'pat\|P}", "exists2 'pat, P & Q", etc.	Hugo Herbelin
2018-02-20	Change default for notations with variables bound to both terms and binders.	Hugo Herbelin
2018-02-20	Notations: Adding modifiers to tell which kind of binder a constr can parse.	Hugo Herbelin
2018-02-20	Notations: A step in cleaning constr_entry_key.	Hugo Herbelin
2018-02-20	Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.	Hugo Herbelin
2018-02-20	More flexibility in locating or referring to a notation.	Hugo Herbelin
2018-02-20	More structured printing in unicode notations for binders.	Hugo Herbelin
2018-02-20	Being more flexible on format Adding a warning to be more informative	Hugo Herbelin
2018-02-20	User-level support for Gonthier-Ssreflect's "if t then pat then u else v".	Hugo Herbelin
2018-02-20	When printing a notation with "match", more flexibility in matching equations.	Hugo Herbelin
2018-02-20	Adding general support for irrefutable disjunctive patterns.	Hugo Herbelin
2018-02-20	Using an "as" clause when needed for printing irrefutable patterns.	Hugo Herbelin
2018-02-20	Refining the strategy for glueing let-ins to a sequence of binders.	Hugo Herbelin
2018-02-20	A (significant) simplification in printing notations with recursive binders.	Hugo Herbelin
2018-02-20	Respecting the ident/pattern distinction in notation modifiers.	Hugo Herbelin
2018-02-20	A first step at refreshing and documenting the new feature.	Hugo Herbelin
2018-02-20	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin
2018-02-20	Adding patterns in the category of binders for notations.	Hugo Herbelin
2018-02-20	Preliminary work before adding general support for patterns in notations II.	Hugo Herbelin
2018-02-20	Preliminary work before adding general support for patterns in notations I.	Hugo Herbelin
2018-02-20	Preliminary work before extending support for binders in notations	Hugo Herbelin
2018-02-20	Preliminary steps before adding general support for patterns in notations.	Hugo Herbelin
2018-02-20	In printing notations with "match", reasoning up to the order of clauses.	Hugo Herbelin