index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
/
ppconstr.ml
Commit message (
Expand
)
Author
Age
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Printing evar instance in a more intuitive order.
Hugo Herbelin
2014-09-29
*
Checking typability of evar instances. Using ";" to separate bindings
Hugo Herbelin
2014-09-13
*
Parsing evar instances.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-09-08
*
A couple of fixes/improvements in -beautify, but backtracking on
Hugo Herbelin
2014-08-12
*
Preliminary re-installation of notation interpretation in beautifying mode.
Hugo Herbelin
2014-08-05
*
Fixing a few beautifying bugs.
Hugo Herbelin
2014-08-05
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
- Better parsing and printing of named universes: Type{ident} and foo@{(ident...
Matthieu Sozeau
2014-06-04
*
- Allow parsing of @const@{instance} for specifying universe instances of pol...
Matthieu Sozeau
2014-06-04
*
- Fix hashing of levels to get the "right" order in universe contexts etc...
Matthieu Sozeau
2014-06-04
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Removing more association lists in Constrintern.
ppedrot
2013-09-02
*
Modules and ppvernac, sequel of Enrico's commit 16261
letouzey
2013-03-13
*
More monomorphization.
ppedrot
2013-03-05
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Yet a new reduction tactic in Coq : cbn
pboutill
2012-12-21
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-10-04
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Avoid Pp.std_ppcmds in Misctypes.sort_info
letouzey
2012-08-07
*
Bigint: avoid dependency over Pp
letouzey
2012-07-30
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Fixing some inconsistencies of constr printer wrt constr parser
herbelin
2012-06-19
*
Internalization of pattern is done in two phases.
pboutill
2012-06-14
*
place all pretty-printing files in new dir printing/
letouzey
2012-05-29