diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-24 17:53:36 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-24 17:53:36 +0100 |
| commit | 9e29a351fd0928130fa0b67dc47b67cdf989e4b7 (patch) | |
| tree | 4da1b4e4a40c1b5905c5d0d08342bf9e839db6d9 /src/translation/HTLgen.v | |
| parent | e60d6c39dd960da14383a823a382e55f88258588 (diff) | |
| download | vericert-9e29a351fd0928130fa0b67dc47b67cdf989e4b7.tar.gz vericert-9e29a351fd0928130fa0b67dc47b67cdf989e4b7.zip | |
Fixes to make develop compile
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 => |