aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.ml
Commit message (Expand)AuthorAge
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* Relaxing the constraint on eta-expanding on the fly while looking forGravatar herbelin2013-05-05
* Fixup notation printing in patternsGravatar pboutill2013-01-07
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Fixup implicits in patterns & notationsGravatar pboutill2012-07-20
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Constrextern is allow to use partially applied notationsGravatar pboutill2012-06-14
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29