The Coq translator incorrectly translates globals that are not applied

[eddywestbrook]

The Coq translator currently does not add module names when it translates globals not in the module where they were defined if they are not applied to arguments.

For example, consider the following SAW core definition in a module other than the prelude:

my_sym : (a : sort 1) -> (x y : a) -> Eq a x y -> Eq a y x;
my_sym = sym;

This is translated to Coq as follows:

Definition my_sym : forall (a : Type), forall (x : a), forall (y : a), SAWCoreScaffolding.Eq a x y -> SAWCoreScaffolding.Eq a y x :=
  fun (a : Type) => sym a.

The call to sym in the above causes an error, because it is actually supposed to refer to SAWCorePrelude.sym. If instead we translate the following definition:

my_sym : (a : sort 1) -> (x y : a) -> Eq a x y -> Eq a y x;
my_sym a = sym a;

then we get the correct result:

Definition my_sym : forall (a : Type), forall (x : a), forall (y : a), SAWCoreScaffolding.Eq a x y -> SAWCoreScaffolding.Eq a y x :=
  fun (a : Type) => SAWCorePrelude.sym a.

The difficulty is likely because of the different code paths in Verifier.SAW.Translation.Coq.Term for translating Constants and ExtCnss than for translating applications whose function component is a global.