aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.ml
Commit message (Expand)AuthorAge
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
* Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
* Fixing a bug in printing the body of a located notation.Gravatar Hugo Herbelin2018-05-13
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Gravatar Maxime Dénès2018-04-12
|\
* | Fixes #7110 ("as" untested while looking for notation for nested patterns).Gravatar Hugo Herbelin2018-03-29
| * [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
|/
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
| * 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
|/
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 09:26:01 +0000