aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation_term.ml')
-rw-r--r--interp/notation_term.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 4e9b8bbb17..82238b71b7 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -45,6 +45,7 @@ type notation_constr =
| NCast of notation_constr * notation_constr cast_type
| NInt of Uint63.t
| NFloat of Float64.t
+ | NArray of notation_constr array * notation_constr * notation_constr
(** Note concerning NList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted