From 816ff701ed0e448fccf0b19cfc08a91ace49123d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 00:12:18 +0100 Subject: progress moving to list of items --- backend/CSE3analysisproof.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend/CSE3analysisproof.v') 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. -- cgit