aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorbarras2003-12-24 10:27:08 +0000
committerbarras2003-12-24 10:27:08 +0000
commit38734c5e122e9a38cf5b8afc586f47abced11361 (patch)
tree2227afa958bf809d9152b526e29f183b552e5e61 /scripts
parentc69ae2a1f05db124c19b7f326ca23e980f643198 (diff)
changement de pose en set (pose n'etait pas utilise avec la semantique
documentee). Reste a retablir la semantique de pose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions