aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Integer/TreeMod
diff options
context:
space:
mode:
authoraspiwack2008-02-29 19:24:57 +0000
committeraspiwack2008-02-29 19:24:57 +0000
commit50d4df2da89461f280c302d032422856f8e77991 (patch)
tree01e93ea00fd08ae5d46add22d72679cd28e0aff4 /theories/Numbers/Integer/TreeMod
parent855cc609d2888ef59d848ed688f02390811b28c7 (diff)
Petite modif pour pouvoir faire "intros until 0" qui introduit autant
que possible des variables qui ont déjà un nom joli tout plein. La conséquence c'est qu'on peut aussi faire "destruct 0" qui est vachement moins intéressant... Mais bon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10610 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/TreeMod')
0 files changed, 0 insertions, 0 deletions