restoring stateful helper proofs

rems-project · Jan 31, 2024 · 4a33abd · 4a33abd
1 parent a50bf93
commit 4a33abd
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -2893,8 +2893,6 @@ Module RevocationProofs.
       Admitted.
 
   End repr_same_proof.
-
-(*
   Opaque CheriMemoryWithPNVI.repr CheriMemoryWithoutPNVI.repr.
 
   (* --- Stateful proofs below --- *)
@@ -3254,7 +3252,6 @@ Module RevocationProofs.
     |[|- Same eq (put _) (put _)] => apply put_Same
     |[|- Same eq (ErrorWithState.update _) (ErrorWithState.update _)] => apply update_Same
     end.
- *)
 
 
   Section allocator_proofs.