aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/interactive
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-09-23 09:36:05 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-09-23 09:36:05 +0000
commit3a4e701b78c0422b019bbac3ea39198126de0677 (patch)
tree570e25139303f4bd0923ab5879e9b081d83a6c08 /test-suite/interactive
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 'test-suite/interactive')
0 files changed, 0 insertions, 0 deletions