summaryrefslogtreecommitdiff
path: root/compiler/SymbolicAst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/SymbolicAst.ml')
-rw-r--r--compiler/SymbolicAst.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 7252a020..cc74a16b 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -141,7 +141,7 @@ type expression =
The context is the evaluation context from after evaluating the asserted
value. It has the same purpose as for the {!Return} case.
*)
- | EvalGlobal of global_decl_id * symbolic_value * expression
+ | EvalGlobal of global_decl_id * generic_args * symbolic_value * expression
(** Evaluate a global to a fresh symbolic value *)
| Assertion of Contexts.eval_ctx * typed_value * expression
(** An assertion.
@@ -251,8 +251,7 @@ and value_aggregate =
| VaCgValue of const_generic_var_id
(** This is used when evaluating a const generic value: in the interpreter,
we introduce a fresh symbolic value. *)
- | VaTraitConstValue of trait_ref * generic_args * string
- (** A trait constant value *)
+ | VaTraitConstValue of trait_ref * string (** A trait constant value *)
[@@deriving
show,
visitors