aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/CombineOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/CombineOp.v')
-rw-r--r--ia32/CombineOp.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v
index ca54ba1b..cdd16071 100644
--- a/ia32/CombineOp.v
+++ b/ia32/CombineOp.v
@@ -10,7 +10,7 @@
(* *)
(* *********************************************************************)
-(** Recognition of combined operations, addressing modes and conditions
+(** Recognition of combined operations, addressing modes and conditions
during the [CSE] phase. *)
Require Import Coqlib.