coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix parsing of :>> and backtrack correctly on the cache of hints for local co...	msozeau	2011-11-18
*	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin	2011-11-17
*	Merge fix for bug #2604.	msozeau	2011-11-17
*	Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due...	msozeau	2011-11-17
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Was missing a potential application of subtyping	msozeau	2011-11-17
*	Fixing tactic remember not correctly checking preservation of typing	herbelin	2011-11-06
*	Auto: removal of ?use_core_db obsolete now that we have nocore	letouzey	2011-11-04
*	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
*	Auto: avoid storing clausenv (and hence env, evar_map, universes) in vo	letouzey	2011-10-26
*	Applying Tom Prince's patch to support parametric "constructor n" in	herbelin	2011-10-25
*	Use full conversion for checking type of holes in destruct over a	herbelin	2011-10-22
*	Fixing Equality.injectable which did not detect an equality without	herbelin	2011-10-22
*	Fix bug #2473 due to wrong folding of the evar environment	msozeau	2011-10-18
*	Fix bug #2227	msozeau	2011-10-18
*	Fix bug #2586 and enhance clsubst* as well as a side effect	msozeau	2011-10-18
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	A new tactic is_var to check whether a term is a goal/section variable	letouzey	2011-10-07
*	When a pattern match, don't use the first matching term but an	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
*	auto with nocore : disable the use of the core database (wish #2188)	letouzey	2011-09-23
*	Remove duplicated version of check_required_library.	letouzey	2011-09-22
*	Tactics.compute_scheme_signature: factorize the two almost-similar cases	letouzey	2011-08-22
*	Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)	aspiwack	2011-08-16
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	Exported tactic intro_then	herbelin	2011-08-10
*	Fix implementation of Hint Immediate used by typeclasses eauto	msozeau	2011-08-10
*	generic = on named_context replaced by named_context_equal	puech	2011-07-29
*	Tactics: replace generic = on constr by destructors	puech	2011-07-29
*	Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ord	puech	2011-07-29
*	Tactics: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Class_tactics: generic equality on named_context_val replaced by eq_named_con...	puech	2011-07-29
*	Eqschemes: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Equality: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tactics: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Equality: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tactics: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tactics: generic equality on named_declaration replaced by eq_named_declaration	puech	2011-07-29
*	Hipattern: two generic equalities on constr spotted & rewritten	puech	2011-07-29
*	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin	2011-07-18
*	Changed name of internally defined "_sym" scheme to avoid confusion with Logi...	herbelin	2011-07-16
*	Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...	herbelin	2011-07-16
*	Relaxed the constraint introduced in r14190 that froze the existing	herbelin	2011-06-18
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	A few comments and a dev file to summarize issues with unification	herbelin	2011-06-13