coq - The formal proof system

Age	Commit message (Expand)	Author
2011-12-12	Proof using ...	gareuselesinge
2011-11-29	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-28	Term: Fix hash_constr behavior for Cast lnterleaved in application spines.	puech
2011-11-21	Typo	herbelin
2011-10-26	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-25	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey
2011-10-24	Mod_subst: Attempt to fix #2608	letouzey
2011-10-11	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-10	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-08	Rely on kernel to know if a name is already used so as to be consistent with it.	herbelin
2011-10-05	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-02	Hash-consing of constr could share more	letouzey
2011-09-25	Polishing commits r14492, r14448 and r14407 (tactics propagate	herbelin
2011-09-24	Completing r14448 and thus continuing r14407 (using Cast to propagate	herbelin
2011-09-22	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-15	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey
2011-09-08	More twicks on hash-consing	letouzey
2011-09-07	Fix the hconsing of universes	letouzey
2011-09-04	Having added a special Cast for remembering the use of conversion	herbelin
2011-08-10	Propagated information from the reduction tactics to the kernel so	herbelin
2011-08-08	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-01	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-07-29	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-04	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey
2011-05-17	Modops: the strengthening functions can work without any env argument	letouzey
2011-05-11	Print Module (Type) M now tries to print more details	letouzey