aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorherbelin2006-09-23 09:36:05 +0000
committerherbelin2006-09-23 09:36:05 +0000
commit3a4e701b78c0422b019bbac3ea39198126de0677 (patch)
tree570e25139303f4bd0923ab5879e9b081d83a6c08 /dev
parent9936e2ba36e1d16dcee047d34b0c4caf8c377726 (diff)
Déplacement surround dans util.ml et parenthésage des déclarations
castées si aussi suivies de leur type (p.ex. dans les hypothèses de but), afin d'éviter des configurations non réinterprétables comme x:nat:nat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9164 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions