diff options
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 66170bc..eb2ddda 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -559,7 +559,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 := +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 => |