aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/interp.mllib
Commit message (Expand)AuthorAge
* [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
* Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atGravatar Pierre-Marie Pédrot2013-12-22
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* Avoid Dumpglob dependency on LexerGravatar letouzey2012-05-29
* Basic stuff about constr_expr migrated from topconstr to constrexpr_opsGravatar letouzey2012-05-29
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20