Added GenerationProofs.v back in the build

QuickChick · Jun 6, 2015 · 7768d92 · 7768d92
1 parent cf1630d
commit 7768d92
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Make b/Make
@@ -20,10 +20,10 @@ Shrinking.v
 SingleStateArb.v
 SSNI.v
 GenerationProofsHelpers.v
-#GenerationProofs.v
+GenerationProofs.v
 #SSNICheckerProofs.v
 NotionsOfNI.v
-#Driver.v
+#Driver.v -- run `make tests` for this
 -I compcert/lib
 compcert/lib/Coqlib.v
 compcert/lib/Integers.v
diff --git a/NIProof.v b/NIProof.v
@@ -699,7 +699,7 @@ Lemma pc_eqS pc pc' l1 l2 :
   (PAtm (BinInt.Z.add pc 1) l1 == PAtm (BinInt.Z.add pc' 1) l2) =
   (PAtm pc l1 == PAtm pc' l2).
 Proof.
-SearchAbout BinInt.Z.add.
+(* SearchAbout BinInt.Z.add. *)
 destruct (PAtm pc l1 == PAtm pc' l2) eqn:Eq.
 + move : Eq.
   move/eqP.