Merge branch 'develop' into arrays-proof

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