aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorherbelin2004-12-29 23:15:03 +0000
committerherbelin2004-12-29 23:15:03 +0000
commite7707310e3138c4fc455d26d5b06f372a5760bdd (patch)
treed534f49850754e03e6b6d08a2e9d8f828adcd993 /dev
parentbcd079c448c946270cbf3c5323ac8cf185450b5f (diff)
ExtraRedExpr maintenant sans argument: pas très souple mais au moins convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions