index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
/
rewrite.v
Commit message (
Expand
)
Author
Age
*
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