coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Extend the computation of dependencies in pattern-matching compilation	herbelin	2011-11-21
*	Add matching on non-inductive types in building an inversion problem	herbelin	2011-11-21
*	Old naming bug in pattern-matching compilation: names in the	herbelin	2011-11-21
*	Inlining let-in (i.e. trace of aliases) in extract_predicate for what	herbelin	2011-11-21
*	In pattern-matching compilation, now taking into account the dependencies	herbelin	2011-11-21
*	Optimizing the compilation of unused aliases in pattern-matching.	herbelin	2011-11-21
*	Simplifying history management in pattern-matching compilation.	herbelin	2011-11-21
*	Fixing postprocessing bugs in pattern-matching compilation.	herbelin	2011-11-21
*	Removing stuff about alias dependencies now become useless.	herbelin	2011-11-21
*	Changed the way to detect if an "as" patterns is expanded or not. The	herbelin	2011-11-21
*	Dead code + refreshing some comments in cases.ml.	herbelin	2011-11-21
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Fix for subclasses implementation, allowing to register generalized classes s...	msozeau	2011-11-18
*	Fixing new bug introduced in r14665 when fixing bug #1834.	herbelin	2011-11-17
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Adding postprocessing to remove "commutative cuts" expansions in	herbelin	2011-11-16
*	Changed the way find_dependencies_signature is working so that it	herbelin	2011-11-16
*	De Bruijn indices bug in pattern matching compilation in the presence	herbelin	2011-11-16
*	Old generalization bug in pattern-matching: names were considered the	herbelin	2011-11-16
*	Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).	herbelin	2011-11-16
*	Old typing bug in pattern-matching compilation (apparently w/o	herbelin	2011-11-16
*	Specialization of tomatch in pattern-matching compilation was done too	herbelin	2011-11-16
*	A bit of documentation around cases.ml + ML modules uselessly open	herbelin	2011-11-16
*	Fixing dependencies lifting bug in pattern-matching compilation	herbelin	2011-11-16
*	Refined second_order_matching so that a constraint on which	herbelin	2011-11-08
*	optimization: memoization for is_open_canonical_projection	gareuselesinge	2011-11-08
*	Improved check is_open_canonical_projection	gareuselesinge	2011-11-08
*	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey	2011-11-07
*	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin	2011-11-06
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Deactivating second-order pattern-matching in evarconv for 8.4.	herbelin	2011-10-26
*	When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty	letouzey	2011-10-26
*	Fixing use of type constraint for refining the "return" clause of "match".	herbelin	2011-10-25
*	Continuing r14585 (ill-typed restriction bug).	herbelin	2011-10-25
*	Continuing r1492 (useless changes were inadvertantly committed)	herbelin	2011-10-25
*	New strategy to infer return predicate of match construct when	herbelin	2011-10-25
*	Still more unification in typing.ml	herbelin	2011-10-25
*	More unification in type_of and addition of e_type_of to get the new	herbelin	2011-10-24
*	Fixing another bug revealing ill-typed use of evar restriction.	herbelin	2011-10-24
*	Fixing instance/filter mismatch in materialize_evar + documentation.	herbelin	2011-10-24
*	Fail if some conv pbs remain after consider_remaining_unif_problems.	herbelin	2011-10-22
*	Now consider remaining conversion problems in solve_remaining_evars.	herbelin	2011-10-22
*	Use also second-order unification if first-order fails at the time of conside...	herbelin	2011-10-22
*	Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...	herbelin	2011-10-22
*	Partly reverting r14539 about fully expanding "let-in"s and not just	herbelin	2011-10-17
*	Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed	herbelin	2011-10-11
*	Unification in the return clause of match was not supported in solve_evars.	herbelin	2011-10-11
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	More on r14536 (an unused pattern-matching remained in the commit).	herbelin	2011-10-11