coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	More robust and uniform treatment of aliases in evarutil.ml	herbelin	2011-10-10
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	Fixing buggy abberant code for Evarutil.expand_evar	herbelin	2011-10-10
*	Little code simplification of instantiate_evar in evd.ml	herbelin	2011-10-10
*	Added information about evar origin in pretty-printing evd for debug	herbelin	2011-10-10
*	Passed conv_algo to evar_define and move call to solve_refl to	herbelin	2011-10-10
*	Fix bug #2557 and an issue with Propers for complement	msozeau	2011-10-07
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	Generalizing subst_term_occ so that it supports an arbitrary matching	herbelin	2011-09-26
*	Adding subst_term up to conv	herbelin	2011-09-26
*	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin	2011-09-26
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	Two bugs in pattern-matching compilation:	herbelin	2011-08-08
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau	2011-08-04
*	Fix nf_evars_undefined	msozeau	2011-08-03
*	Patch to simplify is_open_canonical_projection	herbelin	2011-08-02
*	More robust evar_map debugging printer	herbelin	2011-08-02
*	Evarutil: replace generic list_distinct on constr by constr_list_distinct	puech	2011-07-29
*	Evarutil: replaced some generic = on constr by destructors	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by destructors	puech	2011-07-29
*	Evarconv: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Cases: generic equality on constr replaced by destructors	puech	2011-07-29
*	Classops: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr (x2)	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tacred: generic equality on constr replaced by eq_constr	puech	2011-07-29