aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.ml
Commit message (Expand)AuthorAge
* Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Gravatar Hugo Herbelin2018-02-23
* Notations: Adding modifiers to tell which kind of binder a constr can parse.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
* 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
* 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
* 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
* Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
* Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.Gravatar Hugo Herbelin2017-09-12
* Fixing a typo in printing notations with recursive binders.Gravatar Hugo Herbelin2017-09-12
* Fixing a bug of recursive notations introduced in dfdaf4de.Gravatar Hugo Herbelin2017-09-12
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Adapting code to renaming Array.fold_map -> Array.fold_left_map.Gravatar Hugo Herbelin2017-08-29
* Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| |\
| * | Fix Bug #5568, no dup notation warnings on repeated module importsGravatar Paul Steckler2017-06-09
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\| |
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* | | Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \
| | | * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| | |/
| * | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
* | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
|/ /
* | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-11 06:32:41 +0000