aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.mli
Commit message (Expand)AuthorAge
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29