aboutsummaryrefslogtreecommitdiff
path: root/pretyping/glob_ops.mli
AgeCommit message (Expand)Author
2016-01-20Update copyright headers.Maxime Dénès
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-03-24Fixing equality of notation_constrs. Fixes bug #4136.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-19Glob-ops: a name-mapping operation for pattern-matching binders.Arnaud Spiwack
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-03-02Adding an equality function over glob_constrPierre-Marie Pédrot
2013-04-29Merging Context and Sign.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-11-23Added a constr_pattern_eqppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 14:15:54 +0000