aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
Commit message (Expand)AuthorAge
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
* More monomorphization.Gravatar ppedrot2013-03-05
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* 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
* Avoid Pp.std_ppcmds in Misctypes.sort_infoGravatar letouzey2012-08-07
* Bigint: avoid dependency over PpGravatar letouzey2012-07-30
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Fixing some inconsistencies of constr printer wrt constr parserGravatar herbelin2012-06-19
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29