Fixes

AU-COBRA · Jun 7, 2024 · 28f5fd6 · 28f5fd6
1 parent c398982
commit 28f5fd6
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -7,7 +7,7 @@
 
 theories/hacspec/Hacspec_helpers.v
 theories/hacspec/Hacspec_ovn_Ovn_traits.v
-theories/hacspec/Hacspec_ovn_Ovn_z_89_.v
+#theories/hacspec/Hacspec_ovn_Ovn_z_89_.v
 theories/hacspec/Hacspec_ovn.v
 theories/hacspec/Hacspec_ovn_to_sigma.v
 

diff --git a/theories/hacspec/Hacspec_ovn_to_sigma.v b/theories/hacspec/Hacspec_ovn_to_sigma.v
@@ -69,10 +69,10 @@ Import GroupScope GRing.Theory.
 
 Import PackageNotation.
 
-From Hammer Require Import Reflect.
+(* From Hammer Require Import Reflect.
 From Hammer Require Import Hammer.
 Hammer_version.
-Hammer_objects.
+Hammer_objects. *)
 
 (* Set Hammer Z3. *)
 (* Unset Hammer Parallel. *)
@@ -82,7 +82,7 @@ Hammer_objects.
 (* Set Hammer ATPLimit 30. *)
 (* Hammer_cleanup. *)
 
-Require Import SMTCoq.SMTCoq.
+(* Require Import SMTCoq.SMTCoq. *)
 (* Set SMT Solver "z3". (** Use Z3, also "CVC4" **) *)
 
 Module Misc.
@@ -3023,4 +3023,4 @@ Module OVN_proof (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperation
 
   Admitted.
 
-End OVN_or_proof.
+End OVN_proof.