aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
...
* | | | Refactor impargs code.Gravatar Jasper Hugunin2018-04-05
| * | | Fix #7124: Warning "Ignoring implicit status" does not provide line numberGravatar Maxime Dénès2018-04-05
|/ / /
* | | Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Gravatar Hugo Herbelin2018-04-04
|\ \ \
| * | | Fix #6257: anomaly with Printing Projections and Context.Gravatar Gaëtan Gilbert2018-03-30
| | * | Fixes #7110 ("as" untested while looking for notation for nested patterns).Gravatar Hugo Herbelin2018-03-29
| |/ /
* / / Patterns: Accepting patterns in PFix and PCofix and not only constr.Gravatar Hugo Herbelin2018-03-28
|/ /
| * [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
|/
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Gravatar Maxime Dénès2018-03-09
* Merge PR #6905: Fix make ml-docGravatar Maxime Dénès2018-03-07
|\
* \ Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \
| | * Fix formatting of some ocamldoc comments to reduce warningsGravatar mrmr19932018-03-05
| |/ |/|
| * Allow universe declarations for [with Definition].Gravatar Gaëtan Gilbert2018-03-05
* | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ | |/ |/|
* | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \
| * | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
* | | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
|/ /
* | Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...Gravatar Maxime Dénès2018-02-28
|\ \
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
| * Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Gravatar Hugo Herbelin2018-02-23
* | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
|/
* 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
* More flexibility in locating or referring to a notation.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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 10:43:24 +0000