aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-09 15:42:49 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-09 15:42:49 +0000
commit15da5979d322c5da5f251dfd92da26407df5e45f (patch)
treee523eaad6988c9731fc8868bb20f234ce7934120 /Makefile
parentd63861313993ed3d0a0108d659e0b08a215442c1 (diff)
retour en arriere concernant la recherche d'occurence modulo expansion des letins, ce qui conduisait a des comportement peu intuitifs. On priviligiera l'utilisation de la tactique Subst.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions