coq - The formal proof system

Age	Commit message (Expand)	Author
2018-02-23	Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).	Hugo Herbelin
2018-02-20	Notations: Adding modifiers to tell which kind of binder a constr can parse.	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	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
2018-02-20	Supporting recursive notations reversing the left-to-right order.	Hugo Herbelin
2018-02-20	Allowing variables used in recursive notation to occur several times in pattern.	Hugo Herbelin
2018-02-20	Allows recursive patterns for binders to be associative on the left.	Hugo Herbelin
2018-02-20	A bit of miscellaneous code documentation around notations.	Hugo Herbelin
2018-02-20	Notations: documenting structure collecting variables occurring in notation.	Hugo Herbelin
2018-02-20	More precise explanation when a notation is not reversible for printing.	Hugo Herbelin
2018-02-20	Adding support for re-folding notation referring to isolated "forall '(x,y), t".	Hugo Herbelin
2018-01-30	Use r.(p) syntax to print primitive projections.	Maxime Dénès
2017-11-23	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès
2017-11-13	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias
2017-09-28	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot
2017-09-12	Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.	Hugo Herbelin
2017-09-12	Fixing a typo in printing notations with recursive binders.	Hugo Herbelin
2017-09-12	Fixing a bug of recursive notations introduced in dfdaf4de.	Hugo Herbelin
2017-09-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
2017-08-29	Adapting code to renaming Array.fold_map -> Array.fold_left_map.	Hugo Herbelin
2017-08-29	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin
2017-07-04	Merge branch 'v8.6'	Pierre-Marie Pédrot
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-15	Merge PR#713: Bump year in headers.	Maxime Dénès
2017-06-09	Fix Bug #5568, no dup notation warnings on repeated module imports	Paul Steckler
2017-06-08	Merge branch 'v8.6'	Pierre-Marie Pédrot
2017-06-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-06-01	Merge PR#561: Improving the Name API	Maxime Dénès
2017-06-01	Bump year in headers.	Maxime Dénès
2017-05-31	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin
2017-05-31	Fixing #5523 (missing support for complex constructions in recursive notations).	Hugo Herbelin
2017-05-31	Fixing a too lax constraint for finding recursive binder part of a notation.	Hugo Herbelin
2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
2017-05-24	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias
2017-04-27	Remove some unused values and types	Gaetan Gilbert
2017-04-25	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias
2017-04-25	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias
2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
2017-04-24	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias