coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing rewriting in side conditions for "rewrite in " and "rewrite in \|-".	Hugo Herbelin	2018-03-01
*	Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.	Hugo Herbelin	2015-02-23
*	Experimenting using unification when matching evar/meta free subterms	Hugo Herbelin	2014-11-25
*	Fix test-suite script for subst working with let-ins, the following proof was...	Matthieu Sozeau	2014-06-23
*	Simplification and improvement of "subst x" in such a way that it	Hugo Herbelin	2014-05-08
*	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin	2011-11-06
*	Relaxed the constraint introduced in r14190 that froze the existing	herbelin	2011-06-18
*	Restored a "feature" of unification in pre-8.3 (it was used e.g. in a	herbelin	2010-06-25
*	Revision 12557 continued (better rendering of dependent rewrite)	herbelin	2009-12-13
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Correction problème de compil (blast.ml)	herbelin	2008-04-04
*	Correction typo liée au commit 8779 (levait une anomalie)	herbelin	2007-02-21
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	Ajout test dependent rewrite	herbelin	2004-10-27