From 9e29a351fd0928130fa0b67dc47b67cdf989e4b7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 24 Jun 2020 17:53:36 +0100 Subject: Fixes to make develop compile --- src/translation/HTLgen.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/translation/HTLgen.v') 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 => -- cgit