aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--cfrontend/Csyntax.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 914328be..00565309 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -41,7 +41,7 @@ Inductive expr : Type :=
(**r binary arithmetic operation *)
| Ecast (r: expr) (ty: type) (**r type cast [(ty)r] *)
| Eseqand (r1 r2: expr) (ty: type) (**r sequential "and" [r1 && r2] *)
- | Eseqor (r1 r2: expr) (ty: type) (**r sequential "or" [r1 && r2] *)
+ | Eseqor (r1 r2: expr) (ty: type) (**r sequential "or" [r1 || r2] *)
| Econdition (r1 r2 r3: expr) (ty: type) (**r conditional [r1 ? r2 : r3] *)
| Esizeof (ty': type) (ty: type) (**r size of a type *)
| Ealignof (ty': type) (ty: type) (**r natural alignment of a type *)