aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/glob_ops.ml
Commit message (Expand)AuthorAge
...
* 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
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of identifierGravatar ppedrot2012-12-14
* Added a constr_pattern_eqGravatar ppedrot2012-11-23
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* 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
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29