coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Using "Evd.restrict" in tactic clear so as to keep evar names.	Hugo Herbelin	2014-09-13
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	- Fix has_undefined_evars not using its or_sorts argument anymore.	Matthieu Sozeau	2014-08-03
*	Use kernel conversion on terms that contain universe variables during unifica...	Matthieu Sozeau	2014-07-20
*	Add interface function to replace new_Type ()	Matthieu Sozeau	2014-07-14
*	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau	2014-06-20
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	Fixing "clear" in internal_cut_replace: forbid dependencies in the	Hugo Herbelin	2014-06-13
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau	2014-05-09
*	Cleanup code in pretyping/evarutil	Matthieu Sozeau	2014-05-08
*	Fix performance problem with unification in presence of universes (bug #3302)...	Matthieu Sozeau	2014-05-08
*	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau	2014-05-06
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	Restore reasonable performance by not allocating during universe checks,	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Better representation of evar filters: we represent the vacuous filters of	Pierre-Marie Pédrot	2014-04-23
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Made Pre_env.lazy_val opaque.	Pierre-Marie Pédrot	2014-02-11
*	Tracking memory misallocation by trying to improve sharing.	Pierre-Marie Pédrot	2014-02-03
*	Using Map.smartmap whenever deemed useful.	Pierre-Marie Pédrot	2014-01-29
*	STM: additional fix for STM + vm_compute	Enrico Tassi	2014-01-07
*	Removing useless meta-related functions.	Pierre-Marie Pédrot	2013-12-03
*	Better heuristic for name generation backward compatibility. We fallback	Pierre-Marie Pédrot	2013-11-30
*	Tentative fix to recover fresh name generation as it was before	Pierre-Marie Pédrot	2013-11-30
*	Factoring: is_section_variable.	Arnaud Spiwack	2013-11-25
*	Less partial applications in Vars, as well as better memory allocation.	ppedrot	2013-11-06
*	Nicer infered names in refine.	aspiwack	2013-11-04
*	push_rel_context: do not rename section variables.	aspiwack	2013-11-02
*	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack	2013-11-02
*	Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.	ppedrot	2013-10-29
*	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot	2013-10-27
*	Removing some generic equalities.	ppedrot	2013-10-22
*	Optimizing evar filters. It seems to cost quite a lot in unification,	ppedrot	2013-10-22
*	Small code cleaning in Evarutil.	ppedrot	2013-10-08
*	Removing useless evar code.	ppedrot	2013-10-06
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot	2013-09-18
*	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot	2013-09-05
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	Replacing lists by sets in clear tactic.	ppedrot	2013-08-25
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Allowing different types of, not to be mixed, generic Stores through	ppedrot	2013-03-12