From 7bc2a5e6d2694f144e49fe60af6ddfd0e8a0aba0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 30 Jun 2021 15:59:25 +0200 Subject: coercions and simplify --- scheduling/BTL_SEsimuref.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/BTL_SEsimuref.v') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 9c84532b..66abe6e1 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -20,7 +20,7 @@ Record ristate := { (** [ris_smem] represents the current smem symbolic evaluations. (we also recover the history of smem in ris_smem) *) - ris_smem: smem; + ris_smem:> smem; (** For the values in registers: 1) we store a list of sval evaluations 2) we encode the symbolic regset by a PTree + a boolean indicating the default sval -- cgit