coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Fixing Equality.injectable which did not detect an equality without	herbelin	2011-10-22
*	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
*	Equality: 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
*	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin	2011-07-18
*	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 discriminate for identity.	herbelin	2011-05-26
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Fixing injection bug #2493 (regression introduced by fixing injection	herbelin	2011-03-05
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	correction of bug #2414 (report of r 13586)	jforest	2010-10-27
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	In the computation of missing arguments for apply, accept that the	herbelin	2010-09-17
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New pass on inductive schemes	herbelin	2010-05-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Improving compatibility between 8.2 and 8.3	herbelin	2010-04-05
*	Applied greenrd's patch to fix bug 2255 (injection failed to	herbelin	2010-03-27
*	Safer, though ad hoc, approach to re-interpretation of the argument of	herbelin	2009-12-28
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Improved strategy for rewriting lemma possibly depending because of evars.	herbelin	2009-12-14
*	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin	2009-12-13
*	Completion of r12580 (better rendering of dependent rewrite and inversion).	herbelin	2009-12-13
*	Revision 12557 continued (better rendering of dependent rewrite)	herbelin	2009-12-13
*	Updated compatibility for rewriting equality proofs that are dependent	herbelin	2009-12-12
*	Improved the rendering of "dependent rewrite" and hence of "inversion"	herbelin	2009-12-12
*	Restored rewriting of JMeq using JMeq_rect and co when the domains are the same	herbelin	2009-12-03
*	Addendum to revision 12501.	herbelin	2009-11-12
*	Backtracking on the use of automatically generated schemes for	herbelin	2009-11-11
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Quick fix for restoring a left-to-right rewriting lemma compatible	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Remove old compatibility stuff (Tacred.nf)	glondu	2009-10-28