coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Fixing another bug with "_" intro pattern.	herbelin	2011-06-10
*	Fixing the "buggy" first_name and prepare multi-induction.	herbelin	2011-06-10
*	Made use of "_" in repeated use of intros_patterns work (with	herbelin	2011-06-10
*	Integrating onLastHypId into intro so that we can get the introduction	herbelin	2011-06-10
*	Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof...	msozeau	2011-06-07
*	Fixing discriminate for identity.	herbelin	2011-05-26
*	Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)	letouzey	2011-05-17
*	More work on error handling	letouzey	2011-05-17
*	Merge branch 'subclasses' into coq-trunk	msozeau	2011-05-05
*	Revert r14078 "Partial backtrack on the support for open terms in destruct/in...	gmelquio	2011-04-28
*	Partial backtrack on the support for open terms in destruct/induction:	gmelquio	2011-04-28
*	Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).	herbelin	2011-04-26
*	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin	2011-04-25
*	Fixed a bug of destruct which was sometimes forgetting local definitions behi...	herbelin	2011-04-24
*	Don't force progress on instance applications, there is always progress when ...	msozeau	2011-04-20
*	This is used in the rippling plugin. This also allows fixing bug #2188.	msozeau	2011-04-20
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	More informative anomaly.	herbelin	2011-04-14