coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Names : check of labels, cleanup, nicer debug display of kn and constant	letouzey	2011-10-11
*	Mod_subst: an unused function	letouzey	2011-10-11
*	More on r14536 (an unused pattern-matching remained in the commit).	herbelin	2011-10-11
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	Hash-consing of mutual_inductive_body (and Univ.constraints)	letouzey	2011-10-10
*	Avoid some re-allocation during hash-cons of dir_path	letouzey	2011-10-10
*	Hash-cons the statically allocated Rels (1 to 16) to themselves	letouzey	2011-10-10
*	Hash-cons of constr : avoid some useless allocations	letouzey	2011-10-10
*	Rely on kernel to know if a name is already used so as to be consistent with it.	herbelin	2011-10-08
*	Fixing critical inductive polymorphism bug found by Bruno.	herbelin	2011-10-05
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
*	Hash-consing of constr could share more	letouzey	2011-10-02
*	Polishing commits r14492, r14448 and r14407 (tactics propagate	herbelin	2011-09-25
*	Completing r14448 and thus continuing r14407 (using Cast to propagate	herbelin	2011-09-24
*	Remove specific hash-consing of Term.types (was unused anyway)	letouzey	2011-09-22
*	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
*	Fix the hconsing of universes	letouzey	2011-09-07
*	Having added a special Cast for remembering the use of conversion	herbelin	2011-09-04
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	Term: fix hash_constr to hash modulo casts & names (like compare_constr)	puech	2011-08-08
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	Term: simplify compare_constr by removing calls to decompose_app	puech	2011-08-01
*	fixed bug 2580. Quick fix: copy emitcodes before patching it	barras	2011-08-01
*	Extraction: replace generic = on mutual_inductive_body by mib_equal	puech	2011-07-29
*	Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Term	puech	2011-07-29
*	Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...	puech	2011-07-29
*	Hahtbl_alt: separate generic combine functions	puech	2011-07-29
*	Environ: generic equality on named_context replaced by named_context_equal	puech	2011-07-29
*	Term: added function eq_named_declaration	puech	2011-07-29
*	Indtypes: remove useless and wrong generic equality test on constr array	puech	2011-07-29
*	Term: slight reorganization of the file	puech	2011-07-29
*	Term_typing, Typeops: replace some generic '=' on constr by eq_constr	puech	2011-07-29
*	Term: Refactoring of hashconsing	puech	2011-07-29
*	argument renaming in liftn (match with usual terminology)	puech	2011-07-29
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Fix thumb2-related build error	glondu	2011-04-19
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Fix merge.	msozeau	2011-04-13
*	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Subtyping: align coqtop behavior concerning opaque csts on coqchk's one	letouzey	2011-04-12
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	A few extra combinators about rel_declaration/named_declaration + a bit of doc	herbelin	2011-04-06
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	CHANGES: a word about recent changes in coqide, about Ctrl-C in vm	letouzey	2011-04-01