aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorherbelin2007-08-29 18:42:33 +0000
committerherbelin2007-08-29 18:42:33 +0000
commite72cb7cb39f69af02097e06d525031c9bb5cbd88 (patch)
treeffe62ddb985602541d646161ad55e3b45fe8b0b9 /kernel
parentbfb2e68ff5587b71de525584deab04d4169d29d7 (diff)
Prise en compte des redéfinitions de variables (définitions locales
triviales en provenance de l'algo de compilation du filtrage) lors du calcul de la projection des variables dans real_clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10103 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions