aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/glob_ops.mli
Commit message (Expand)AuthorAge
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 06:44:37 +0000