summaryrefslogtreecommitdiff
path: root/src/state.ml
diff options
context:
space:
mode:
authorPeter Sewell2018-07-27 18:57:02 +0100
committerPeter Sewell2018-07-27 18:57:02 +0100
commit3755e6701a9286677fd2f4ca40a16305b360f9d9 (patch)
tree67766e537db5bb8dbfc6b59432b2786a88b76be3 /src/state.ml
parent2a35c6b9e1cfac8ce34ef6fa7c264cfea4139002 (diff)
parente4af7c3090c93a129e99dd75f2a20d5a9d2f6920 (diff)
Merge branch 'sail2' of github.com:rems-project/sail into sail2
Diffstat (limited to 'src/state.ml')
-rw-r--r--src/state.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/state.ml b/src/state.ml
index 245d450c..70e53a52 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -69,9 +69,9 @@ let find_registers defs =
List.fold_left
(fun acc def ->
match def with
- | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), annot)) ->
- let env = match annot with
- | (_, Some (env, _, _)) -> env
+ | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), (_, tannot))) ->
+ let env = match destruct_tannot tannot with
+ | Some (env, _, _) -> env
| _ -> Env.empty
in
(Env.expand_synonyms env typ, id) :: acc