coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
*	Improving pretty-printing of Ltac functions.	herbelin	2011-12-17
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Some extra universe refreshing seems needed in abstract_generalize	herbelin	2011-12-14
*	Proof using ...	gareuselesinge	2011-12-12
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	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