Update the proofs of the C front-end to the new linking framework.

1 files changed, 5 insertions, 5 deletions

diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index a5a6ad66..c88c4db5 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -512,9 +512,9 @@ Local Open Scope error_monad_scope.
 
 Definition transl_fundef (fd: Csyntax.fundef) : res fundef :=
   match fd with
-  | Csyntax.Internal f =>
+  | Internal f =>
       do tf <- transl_function f; OK (Internal tf)
-  | Csyntax.External ef targs tres cc =>
+  | External ef targs tres cc =>
       OK (External ef targs tres cc)
   end.
 
@@ -523,6 +523,6 @@ Definition transl_program (p: Csyntax.program) : res program :=
   OK {| prog_defs := AST.prog_defs p1;
         prog_public := AST.prog_public p1;
         prog_main := AST.prog_main p1;
-        prog_types := Csyntax.prog_types p;
-        prog_comp_env := Csyntax.prog_comp_env p;
-        prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}.
+        prog_types := prog_types p;
+        prog_comp_env := prog_comp_env p;
+        prog_comp_env_eq := prog_comp_env_eq p |}.