cond_depends_on

1 files changed, 7 insertions, 7 deletions

diff --git a/x86/Op.v b/x86/Op.v
index e7c910c2..caa63235 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -999,7 +999,7 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
-Definition condition_depends_on_memory (c: condition) : bool :=
+Definition cond_depends_on_memory (c: condition) : bool :=
   match c with
   | Ccompu _ => negb Archi.ptr64
   | Ccompuimm _ _ => negb Archi.ptr64
@@ -1010,14 +1010,14 @@ Definition condition_depends_on_memory (c: condition) : bool :=
 
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp c => condition_depends_on_memory c
-  | Osel c ty => condition_depends_on_memory c
+  | Ocmp c => cond_depends_on_memory c
+  | Osel c ty => cond_depends_on_memory c
   | _ => false
   end.
 
-Lemma condition_depends_on_memory_correct:
+Lemma cond_depends_on_memory_correct:
   forall c args m1 m2,
-  condition_depends_on_memory c = false ->
+  cond_depends_on_memory c = false ->
   eval_condition c args m1 = eval_condition c args m2.
 Proof.
   intros until m2. 
@@ -1031,9 +1031,9 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence; intros C.
-- f_equal; f_equal; apply condition_depends_on_memory_correct; auto.
+- f_equal; f_equal; apply cond_depends_on_memory_correct; auto.
 - destruct args; auto. destruct args; auto.
-  rewrite (condition_depends_on_memory_correct c args m1 m2 C).
+  rewrite (cond_depends_on_memory_correct c args m1 m2 C).
   auto.
 Qed.