Unless I'm misreading this, there's a slight semantic difference between the two cases: with the GADT-based interpreter, an if expression's two branches must both evaluate to integers:

  | GIf : bool expr' * int expr' * int expr' -> int expr'

...whereas in the original both branches could evaluate to bools (or even totally separate types). Do you need a separate case for each type, or could one write something like the following?

  | GIf : bool expr' * a expr' * a expr' -> a expr'