| Age | Commit message (Expand) | Author |
|---|
| 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 | 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 |
| 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 | Renaming binders into binderlists in egramcoq.ml. | Hugo Herbelin |
| 2018-02-20 | Introducing an intermediary type "constr_prod_entry_key" for grammar producti... | Hugo Herbelin |
| 2018-02-20 | Canonically add an encoding in glob_constr of "as" operator for cases_pattern. | 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 | Rephrasing ETBinderList with a self-documenting and invariant-carrying argument. | 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 |
