summaryrefslogtreecommitdiff
path: root/language/l2.ml
diff options
context:
space:
mode:
authorKathy Gray2014-03-26 15:05:11 +0000
committerKathy Gray2014-03-26 15:05:11 +0000
commit9549b13972f5c3173bc7d11ea1b62b490f673166 (patch)
tree79cdaae2139bd76429339e882b830d2f9c5f5124 /language/l2.ml
parent0689a3347e02d92b821ff2a29210681a001efd51 (diff)
More steps towards solving and using constraint information
Diffstat (limited to 'language/l2.ml')
-rw-r--r--language/l2.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/language/l2.ml b/language/l2.ml
index 80c94b39..927f702b 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -282,6 +282,8 @@ and 'a exp_aux = (* Expression *)
| E_case of 'a exp * ('a pexp) list (* pattern matching *)
| E_let of 'a letbind * 'a exp (* let expression *)
| E_assign of 'a lexp * 'a exp (* imperative assignment *)
+ | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
+ | E_internal_exp of 'a annot (* This is an internal use of an nexp (in the annot) for passing length information after resolution of constraints *)
and 'a exp =
E_aux of 'a exp_aux * 'a annot