index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
names.mli
Commit message (
Expand
)
Author
Age
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Missing equalities in Names-like structures.
Pierre-Marie Pédrot
2014-03-20
*
Using HMaps in global references.
Pierre-Marie Pédrot
2014-03-08
*
Also use HMaps in KNmap.
Pierre-Marie Pédrot
2014-03-08
*
Using Hashmaps by default in constant and inductive maps. This changes fold and
Pierre-Marie Pédrot
2014-03-07
*
Inductive maps in Environ now use HMap.
Pierre-Marie Pédrot
2014-03-06
*
Lazily computed hash in KerName.t.
Pierre-Marie Pédrot
2014-03-05
*
Fixing generic hashes and replacing them with proper ones.
Pierre-Marie Pédrot
2014-03-03
*
Allocation-friendly mapping functions in Nametab.
Pierre-Marie Pédrot
2014-02-03
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Specializing hash functions for widely used types.
ppedrot
2013-10-24
*
cList: a few alternative to hashtbl-based uniquize, distinct, subset
letouzey
2013-10-23
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Small fixes due to the arrival of OCaml 3.12.
ppedrot
2013-08-03
*
Replacing Id.check with Id.is_valid, as its sole use was under
ppedrot
2013-05-14
*
Removing Gmap from Extraction plugin
ppedrot
2013-05-12
*
Minor cleanup concerning Mod_subst.MBImap
letouzey
2013-04-02
*
Restrict (try...with...) to avoid catching critical exn (part 1)
letouzey
2013-03-12
*
Names: shortcuts for building {kn, constant, mind} with empty sections
letouzey
2013-02-26
*
Names: Modularize constant and mutual_inductive
letouzey
2013-02-26
*
Dir_path --> DirPath
letouzey
2013-02-19
*
module_path --> ModPath.t, kernel_name --> KerName.t
letouzey
2013-02-19
*
Names: revised representation of constants and mutual_inductive
letouzey
2013-02-19
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Fixing ocalmdoc comment
ppedrot
2012-12-14
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moving hcons_string to String namespace.
ppedrot
2012-12-14
*
Monomorphization (kernel)
ppedrot
2012-11-22
*
More monomorphizations
ppedrot
2012-11-13
*
Removed many calls to OCaml generic equality. This was done by
ppedrot
2012-10-29
*
Updating headers.
herbelin
2012-08-08
*
Noise for nothing
pboutill
2012-03-02
*
Names : check of labels, cleanup, nicer debug display of kn and constant
letouzey
2011-10-11
*
Hash-consing of constr could share more
letouzey
2011-10-02
*
Hash-consing: attempt to stop hash-consing separately constr in declare.ml
letouzey
2011-09-22
*
Names.make_mbid and co : convert from/to identifier (avoid some String.copy)
letouzey
2011-09-15
*
More twicks on hash-consing
letouzey
2011-09-08
*
Print Module (Type) M now tries to print more details
letouzey
2011-05-11
*
Moving printing of module typing errors upwards to himsg.ml so as to
herbelin
2011-03-05
*
compatibility <3.12 (Map.exists Map.singleton)
pboutill
2011-02-11
*
Make simpl use the proper constant when folding (mutual) fixpoints
letouzey
2011-01-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Names: remove obsolete mod_self_id
letouzey
2010-06-23
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
After the approval of Bruno, here the patch for the checker.
soubiran
2010-04-29
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
[next]