aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Csem.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Csem.v')
-rw-r--r--cfrontend/Csem.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 927cd69d..dff5fa26 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -13,7 +13,7 @@
(* *)
(* *********************************************************************)
-(** Dynamic semantics for the Clight language *)
+(** Dynamic semantics for the Compcert C language *)
Require Import Coqlib.
Require Import Errors.