coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Adding newline after warning and restoring distinction between	herbelin	2012-04-15
*	Shortcuts and optimizations of comparisons	xclerc	2012-04-05
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	Univ: switch the order of int and dir_path in UniverseLevel.Level	letouzey	2012-03-22
*	Reorganizing the structure of evarutil.ml (only restructuration, no	herbelin	2012-03-20
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Fixing vm_compute bug #2729 (function used to decompose constructors	herbelin	2012-03-13
*	Univ: avoid recording dummy universe constraints u<=u or u=u	letouzey	2012-03-12
*	Noise for nothing	pboutill	2012-03-02
*	Univ: a univ_depends function to avoid a hack in Inductiveops	letouzey	2012-03-01
*	Univ: a better Constraint.compare	letouzey	2012-03-01
*	Univ: a faster is_leq test used when possible	letouzey	2012-02-29
*	Univ: correct compare_neq (fix #2703)	letouzey	2012-02-27
*	Proof using ...	gareuselesinge	2011-12-12
*	Term: properly ignore Casts between Apps in constr_ord	puech	2011-11-29
*	Term: useless conversion to list in constr_ord deleted	puech	2011-11-29
*	Term: Fix hash_constr behavior for Cast lnterleaved in application spines.	puech	2011-11-28
*	Typo	herbelin	2011-11-21
*	When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty	letouzey	2011-10-26
*	Environ.set_universes is dead code	letouzey	2011-10-26
*	Mod_subst: some simplifications, some more significant names to functions, etc	letouzey	2011-10-26
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	Mod_subst: Attempt to fix #2608	letouzey	2011-10-24
*	Safe_typing: adding a inductive block adds many labels (fix #2603)	letouzey	2011-10-11
*	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