6 files changed, 12 insertions, 9 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 790a6624..70252a1a 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -411,7 +411,8 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
          E_internal_return(to_ast_exp ctx exp)
        else
          raise (Reporting.err_general l "Internal return construct found without -dmagic_hash")
-    | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
+    | P.E_deref exp ->
+       E_app (Id_aux (Id "__deref", l), [to_ast_exp ctx exp])
     ), (l,()))
 
 and to_ast_measure ctx (P.Measure_aux(m,l)) : unit internal_loop_measure =
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index f26c74d7..afa63cb9 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -920,8 +920,7 @@ let doc_lit (L_aux(lit,l)) =
       let denom = Big_int.pow_int_positive 10 (String.length f) in
       (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
     | _ ->
-      raise (Reporting.Fatal_error
-        (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in
+      raise (Reporting.err_syntax_loc l "could not parse real literal") in
     parens (separate space (List.map string [
       "realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
 
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 10441ed5..708749cc 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -423,8 +423,7 @@ let doc_lit_lem (L_aux(lit,l)) =
       let denom = Big_int.pow_int_positive 10 (String.length f) in
       (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
     | _ ->
-      raise (Reporting.Fatal_error
-        (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in
+      raise (Reporting.err_syntax_loc l "could not parse real literal") in
     parens (separate space (List.map string [
       "realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
 
diff --git a/src/reporting.ml b/src/reporting.ml
index c85f20ff..9387ee6b 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -133,7 +133,7 @@ type error =
   | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
   | Err_todo of Parse_ast.l * string
   | Err_syntax of Lexing.position * string
-  | Err_syntax_locn of Parse_ast.l * string
+  | Err_syntax_loc of Parse_ast.l * string
   | Err_lex of Lexing.position * string
   | Err_type of Parse_ast.l * string
 
@@ -145,7 +145,7 @@ let dest_err = function
      (Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line, Loc l, m ^ issues)
   | Err_todo (l, m) -> ("Todo" ^ m, Loc l, "")
   | Err_syntax (p, m) -> ("Syntax error", Pos p, m)
-  | Err_syntax_locn (l, m) -> ("Syntax error", Loc l, m)
+  | Err_syntax_loc (l, m) -> ("Syntax error", Loc l, m)
   | Err_lex (p, s) -> ("Lexical error", Pos p, s)
   | Err_type (l, m) -> ("Type error", Loc l, m)
 
@@ -156,6 +156,7 @@ let err_todo l m = Fatal_error (Err_todo (l, m))
 let err_unreachable l ocaml_pos m = Fatal_error (Err_unreachable (l, ocaml_pos, m))
 let err_general l m = Fatal_error (Err_general (l, m))
 let err_typ l m = Fatal_error (Err_type (l,m))
+let err_syntax_loc l m = Fatal_error (Err_syntax_loc (l, m))
 
 let unreachable l pos msg =
   raise (err_unreachable l pos msg)
diff --git a/src/reporting.mli b/src/reporting.mli
index 86399e84..28f2a799 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -93,7 +93,7 @@ type error =
   | Err_todo of Parse_ast.l * string
 
   | Err_syntax of Lexing.position * string
-  | Err_syntax_locn of Parse_ast.l * string
+  | Err_syntax_loc of Parse_ast.l * string
   | Err_lex of Lexing.position * string
   | Err_type of Parse_ast.l * string
 
@@ -111,6 +111,9 @@ val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
 (** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
 val err_typ : Parse_ast.l -> string -> exn
 
+(** [err_syntax_loc] is an abbreviation for [Fatal_error (Err_syntax_loc (l, m))] *)
+val err_syntax_loc : Parse_ast.l -> string -> exn
+  
 val unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'a
 
 val print_error : error -> unit
diff --git a/src/type_check.ml b/src/type_check.ml
index 0365e2e5..eeb6773b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -902,7 +902,7 @@ end = struct
     try
       Bindings.find id env.top_val_specs
     with
-    | Not_found -> typ_error env (id_loc id) ("No val spec found for " ^ string_of_id id)
+    | Not_found -> typ_error env (id_loc id) ("No type signature found for " ^ string_of_id id)
 
   let get_val_spec id env =
     try