diff options
author | François Pottier <francois.pottier@inria.fr> | 2015-10-07 10:09:33 +0200 |
---|---|---|
committer | François Pottier <francois.pottier@inria.fr> | 2015-10-07 10:24:50 +0200 |
commit | 7c4dd1467e62229689fe15656f4405f617edca1d (patch) | |
tree | 27be05981f54c7f773bd73d08de22fe401c08302 /driver/Compiler.v | |
parent | d9b17759c9a56a33b7e2d57e0aaaab4951ef222d (diff) | |
download | compcert-7c4dd1467e62229689fe15656f4405f617edca1d.tar.gz compcert-7c4dd1467e62229689fe15656f4405f617edca1d.zip |
Introduced [other_identifier] as a more elegant way of calling [set_id_type i OtherId].
This causes no change in the automaton.
Diffstat (limited to 'driver/Compiler.v')
0 files changed, 0 insertions, 0 deletions