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
2015-02-27
Adding a new folder corresponding to the low-level part of the pretyper
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-12-09
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-09-27
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-12
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-08-25
Fixing the essence of naming bug #3204: use same strategy for naming
Hugo Herbelin
2014-08-05
A new step in the new "standard" naming policy for propositional hypotheses
Hugo Herbelin
2014-06-17
Removing dead code.
Pierre-Marie Pédrot
2014-06-04
Collecting in Namegen those conventional default names that are used in diffe...
Hugo Herbelin
2014-06-01
Use of "H"-based names for propositional hypotheses obtained by
Hugo Herbelin
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