index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
namegen.ml
Commit message (
Expand
)
Author
Age
*
Slight improvement in naming anonymous variables in error messages:
Hugo Herbelin
2015-07-16
*
Update headers.
Maxime Dénès
2015-01-12
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Fixing the essence of naming bug #3204: use same strategy for naming
Hugo Herbelin
2014-08-25
*
A new step in the new "standard" naming policy for propositional hypotheses
Hugo Herbelin
2014-08-05
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Collecting in Namegen those conventional default names that are used in diffe...
Hugo Herbelin
2014-06-04
*
Use of "H"-based names for propositional hypotheses obtained by
Hugo Herbelin
2014-06-01
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing List.mem in Namegen. We may choose a better fitted datastructure tha...
ppedrot
2013-10-23
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Nicer code concerning dirpaths and modpath around Lib
letouzey
2013-08-22
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
More cleanup of Util: utf8 aspects moved to a new file unicode.ml
letouzey
2012-09-18
*
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
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-20
*
Noise for nothing
pboutill
2012-03-02
*
Printing bugs with match patterns:
herbelin
2012-01-27
*
Added a table for using reserved names for binding names to types
herbelin
2011-03-05
*
Remove "init" label from Termops.it_mk* specialized functions
glondu
2010-09-28
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)
herbelin
2009-12-03
*
Continuing r12485-12486 (cleaning around name generation)
herbelin
2009-12-01
*
Commit 12485 continued.
herbelin
2009-11-09