aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation/HTLgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r--src/translation/HTLgen.v5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index dc82fb1..e637d6f 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -572,8 +572,7 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
(fun i v => Errors.OK v) p.
*)
-Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true.
-(*
+Definition main_is_internal (p : RTL.program) : bool :=
let ge := Globalenvs.Genv.globalenv p in
match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
| Some b =>
@@ -582,7 +581,7 @@ Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true.
| _ => false
end
| _ => false
- end. *)
+ end.
Definition transl_program (p : RTL.program) : Errors.res HTL.program :=
if main_is_internal p