aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
* Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
* Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
* More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
* More structured printing in unicode notations for binders.Gravatar Hugo Herbelin2018-02-20
* Being more flexible on format Adding a warning to be more informativeGravatar Hugo Herbelin2018-02-20
* User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Gravatar Hugo Herbelin2018-02-20
* When printing a notation with "match", more flexibility in matching equations.Gravatar Hugo Herbelin2018-02-20
* Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
* Using an "as" clause when needed for printing irrefutable patterns.Gravatar Hugo Herbelin2018-02-20
* Refining the strategy for glueing let-ins to a sequence of binders.Gravatar Hugo Herbelin2018-02-20
* A (significant) simplification in printing notations with recursive binders.Gravatar Hugo Herbelin2018-02-20
* Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
* A first step at refreshing and documenting the new feature.Gravatar Hugo Herbelin2018-02-20
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
* Preliminary work before adding general support for patterns in notations II.Gravatar Hugo Herbelin2018-02-20
* Preliminary work before adding general support for patterns in notations I.Gravatar Hugo Herbelin2018-02-20
* Preliminary work before extending support for binders in notationsGravatar Hugo Herbelin2018-02-20
* Preliminary steps before adding general support for patterns in notations.Gravatar Hugo Herbelin2018-02-20
* In printing notations with "match", reasoning up to the order of clauses.Gravatar Hugo Herbelin2018-02-20
* Preliminary work before extending support for binders in notationsGravatar Hugo Herbelin2018-02-20
* Make pattern variables of "match" substitutable in notations.Gravatar Hugo Herbelin2018-02-20
* Supporting recursive notations reversing the left-to-right order.Gravatar Hugo Herbelin2018-02-20
* Allowing variables used in recursive notation to occur several times in pattern.Gravatar Hugo Herbelin2018-02-20
* Allows recursive patterns for binders to be associative on the left.Gravatar Hugo Herbelin2018-02-20
* Fixing/improving notations with recursive patterns.Gravatar Hugo Herbelin2018-02-20
* A bit of miscellaneous code documentation around notations.Gravatar Hugo Herbelin2018-02-20
* Notations: documenting structure collecting variables occurring in notation.Gravatar Hugo Herbelin2018-02-20
* Renaming binders into binderlists in egramcoq.ml.Gravatar Hugo Herbelin2018-02-20
* Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Gravatar Hugo Herbelin2018-02-20
* Canonically add an encoding in glob_constr of "as" operator for cases_pattern.Gravatar Hugo Herbelin2018-02-20
* Minor clarifying of name variables in constrintern.ml.Gravatar Hugo Herbelin2018-02-20
* Using name given by user to name a 'pat, if any.Gravatar Hugo Herbelin2018-02-20
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Gravatar Hugo Herbelin2018-02-20
* Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
* More precise explanation when a notation is not reversible for printing.Gravatar Hugo Herbelin2018-02-20
* Adding support for re-folding notation referring to isolated "forall '(x,y), t".Gravatar Hugo Herbelin2018-02-20
* Again one more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2018-02-20
* Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Gravatar Maxime Dénès2018-02-19
|\
* \ Merge PR #6761: Remove unused argument in Record.declare_structureGravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\ \ \
* \ \ \ Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\ \ \ \
* \ \ \ \ Merge PR #6230: Better Cemitcodes API + compact relocation representationGravatar Maxime Dénès2018-02-19
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6759: detype_case predicate is not optionalGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6772: Cleanup inferCumulativityGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6648: [tactics] make apply_type safeGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 20:17:17 +0000