aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/SelectOpproof.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 63066135..b0cd70a4 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -1095,5 +1095,4 @@ Proof.
intros. discriminate.
Qed.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
End CMCONSTR.