diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 00:12:18 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 00:12:18 +0100 |
| commit | 816ff701ed0e448fccf0b19cfc08a91ace49123d (patch) | |
| tree | ad41a939ccdfd60763e18997319de67b87dc492c /backend/CSE3analysisproof.v | |
| parent | 69e65970df233c88fcfcefd0bb0e5f61a078fb2a (diff) | |
| download | compcert-kvx-816ff701ed0e448fccf0b19cfc08a91ace49123d.tar.gz compcert-kvx-816ff701ed0e448fccf0b19cfc08a91ace49123d.zip | |
progress moving to list of items
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 10ffe760..8cc009cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1288,6 +1288,7 @@ Section SOUNDNESS. Hint Resolve external_call_sound : cse3. + (* Section INDUCTIVENESS. Variable fn : RTL.function. Variable tenv : typing_env. @@ -1348,4 +1349,5 @@ Section SOUNDNESS. End INDUCTIVENESS. Hint Resolve checked_is_inductive_allstep checked_is_inductive_entry : cse3. + *) End SOUNDNESS. |