explicitly set use_full_type_names := false in stateless hol light

makes the translator less likely to fail as its defaults apparently
changed...
Fix type soundness

Show that it gives the no duplicate module/types properties that the new
whole-prog semantics requires.
More fixes toward getting conLangProof cheat free

I think everything that conLang needs to rely on should now be provided
by the modLang semantics.
Merge remote-tracking branch 'origin/master' into conLang_wip
More conLang progress
prove one cheat in prog_to_i2_correct
minor fixes to broken proofs about compile_prog

must have been broken by some recent changes to HOL?
Merge remote-tracking branch 'origin/master' into conLang_wip
fix proof in holAxiomsSyntaxTheory

I believe this is (more) fallout from commit 875ba111 in HOL.
Add some more invariants to the modLang wholeProg semantics
More work on conLangProof

There is now an assumption about prompt_mods_ok at the cheat points.
failing attempt to prove second prog_to_i2_correct cheat

got part of it done though (in tac2)
additions to cakeml_compset for compiling datatype defs
Added a bit more checking to the whole program semantics

Now there is a type error is any type or module in a whole program is
already defined in the initial environment, even if that declaration is
not reached in evaluation.
delta on prog_to_i2_correct
add some cakeml_compset things for structure declarations
translator now knows about modules
translator can now translate into a module
clean up some of the code
derive thm about generated module, demo file