aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/glob_ops.mli
Commit message (Expand)AuthorAge
* Using an "as" clause when needed for printing irrefutable patterns.Gravatar Hugo Herbelin2018-02-20
* Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
* | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * | Adding a fold_glob_constr_with_binders combinator.Gravatar Hugo Herbelin2017-04-13
|/ /
| * Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
|/
* A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
* Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* Fixing equality of notation_constrs. Fixes bug #4136.Gravatar Pierre-Marie Pédrot2015-03-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* Glob-ops: a name-mapping operation for pattern-matching binders.Gravatar Arnaud Spiwack2014-11-19
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Adding an equality function over glob_constrGravatar Pierre-Marie Pédrot2014-03-02
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Added a constr_pattern_eqGravatar ppedrot2012-11-23
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29