Total proof fewer assumptions

AU-COBRA · Sep 8, 2024 · 94d6cc3 · 94d6cc3
1 parent 9df256e
commit 94d6cc3
Show file tree

Hide file tree

Showing 5 changed files with 2,768 additions and 1,126 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -7,12 +7,13 @@ theories/hacspec/Hacspec_ovn.v
 theories/hacspec/Hacspec_ovn_group_and_field.v
 
 theories/hacspec/Hacspec_ovn_sigma_setup.v
+
 theories/hacspec/Hacspec_ovn_schnorr.v
 theories/hacspec/Hacspec_ovn_or.v
 
 theories/ovn/OVN.v
 
-# theories/hacspec/Hacspec_ovn_total_proof.v
+theories/hacspec/Hacspec_ovn_total_proof.v
 # theories/hacspec/Hacspec_ovn_proof_z_89.v
 
 # -R theories/hacspec Examples