diff options
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. |