index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
namegen.ml
Age
Commit message (
Expand
)
Author
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2013-10-23
Removing List.mem in Namegen. We may choose a better fitted datastructure tha...
ppedrot
2013-09-19
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-08-22
Nicer code concerning dirpaths and modpath around Lib
letouzey
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
2013-02-19
Dir_path --> DirPath
letouzey
2012-12-18
Modulification of name
ppedrot
2012-12-18
Modulification of Label
ppedrot
2012-12-14
Modulification of dir_path
ppedrot
2012-12-14
Modulification of identifier
ppedrot
2012-11-22
Monomorphization (pretyping)
ppedrot
2012-09-18
More cleanup of Util: utf8 aspects moved to a new file unicode.ml
letouzey
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-08-08
Updating headers.
herbelin
2012-05-29
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-03-20
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-02
Noise for nothing
pboutill
2012-01-27
Printing bugs with match patterns:
herbelin
2011-03-05
Added a table for using reserved names for binding names to types
herbelin
2010-09-28
Remove "init" label from Termops.it_mk* specialized functions
glondu
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2009-12-03
Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)
herbelin
2009-12-01
Continuing r12485-12486 (cleaning around name generation)
herbelin
2009-11-09
Commit 12485 continued.
herbelin