summaryrefslogtreecommitdiff
path: root/src/initial_check.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/initial_check.ml')
-rw-r--r--src/initial_check.ml10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index d08ab8cf..108e04d0 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -387,6 +387,16 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
| P.E_throw exp -> E_throw (to_ast_exp ctx exp)
| P.E_return exp -> E_return(to_ast_exp ctx exp)
| P.E_assert(cond,msg) -> E_assert(to_ast_exp ctx cond, to_ast_exp ctx msg)
+ | P.E_internal_plet(pat,exp1,exp2) ->
+ if !opt_magic_hash then
+ E_internal_plet(to_ast_pat ctx pat, to_ast_exp ctx exp1, to_ast_exp ctx exp2)
+ else
+ raise (Reporting.err_general l "Internal plet construct found without -dmagic_hash")
+ | P.E_internal_return(exp) ->
+ if !opt_magic_hash then
+ 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")
), (l,()))