aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.mli
Commit message (Expand)AuthorAge
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* 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
* 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
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29