coq - The formal proof system

Age	Commit message (Expand)	Author
2018-02-28	Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...	Maxime Dénès
2018-02-23	Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).	Hugo Herbelin
2018-02-22	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias
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	More flexibility in locating or referring to a notation.	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	Preliminary work before extending support for binders in notations	Hugo Herbelin
2018-02-20	Make pattern variables of "match" substitutable in notations.	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	Fixing/improving notations with recursive patterns.	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	Minor clarifying of name variables in constrintern.ml.	Hugo Herbelin
2018-02-20	Using name given by user to name a 'pat, if any.	Hugo Herbelin
2018-02-20	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin
2018-02-20	Notations: Do not consider a non-occurring variable as a binder-only variable.	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-02-20	Again one more step in fixing #5762 ("where" clause).	Hugo Herbelin
2018-02-16	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot
2018-02-12	Merge PR #1047: Support universe instances on the literal Type	Maxime Dénès
2018-02-12	Merge PR #6128: Simplification: cumulativity information is variance informa...	Maxime Dénès
2018-02-11	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert
2018-02-10	Inference of inductive subtyping does not need an evar map.	Gaëtan Gilbert
2018-02-10	Simplification: cumulativity information is variance information.	Gaëtan Gilbert
2018-01-30	Use r.(p) syntax to print primitive projections.	Maxime Dénès
2018-01-26	Support universe instances on the literal Type	Tej Chajed
2018-01-08	Merge PR #6532: Fix mli-doc issue #6531	Maxime Dénès
2018-01-01	Fix mli-doc issue #6531	Tony Beta Lambda
2017-12-30	Using a dedicated type for Lib.abstr_info.	Pierre-Marie Pédrot
2017-12-27	Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.	Maxime Dénès
2017-12-27	Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...	Maxime Dénès
2017-12-23	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias
2017-12-22	Merge PR #6469: No universe constraints in Let definitions	Maxime Dénès