3 files changed, 15 insertions, 2 deletions
diff --git a/src/sail.ml b/src/sail.ml
index a7f780b9..9208190d 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -109,7 +109,7 @@ let options = Arg.align ([
     Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators),
     "<types> produce random generators for the given types");
   ( "-latex",
-    Arg.Set opt_print_latex,
+    Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ],
     " pretty print the input to latex");
   ( "-c",
     Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen],
diff --git a/src/type_check.ml b/src/type_check.ml
index 46b67930..4ad93a0c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -73,6 +73,10 @@ let opt_no_lexp_bounds_check = ref false
    definitions *)
 let opt_constraint_synonyms = ref false
 
+(* opt_expand_valspec expands typedefs in valspecs during type check.
+   We prefer not to do it for latex output but it is otherwise a good idea. *)
+let opt_expand_valspec = ref true
+
 let depth = ref 0
 
 let rec indent n = match n with
@@ -4337,7 +4341,12 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
        in
        let env = Env.add_extern id ext_opt env in
        let env = if is_cast then Env.add_cast id env else env in
-       let typq, typ = expand_bind_synonyms ts_l env (typq, typ) in
+       let typq, typ =
+         if !opt_expand_valspec then 
+           expand_bind_synonyms ts_l env (typq, typ)
+         else
+           (typq, typ)
+       in
        let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in
        (vs, id, typq, typ, env)
   in
diff --git a/src/type_check.mli b/src/type_check.mli
index 1cb54770..dc1cfe97 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -71,6 +71,10 @@ val opt_no_lexp_bounds_check : bool ref
    definitions *)
 val opt_constraint_synonyms : bool ref
 
+(** opt_expand_valspec expands typedefs in valspecs during type check.
+   We prefer not to do it for latex output but it is otherwise a good idea. *)
+val opt_expand_valspec : bool ref
+
 (** {2 Type errors} *)
 
 type type_error =