diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-17 18:21:19 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-17 18:21:19 +0100 |
| commit | ea64d739af16952883abce536958ac4877698277 (patch) | |
| tree | 090752ca05d8b747270f152351849801b6e92f50 /src | |
| parent | 4f074002b6c2b626a3f41528e9b3bdf62b82e2bc (diff) | |
| download | vericert-kvx-ea64d739af16952883abce536958ac4877698277.tar.gz vericert-kvx-ea64d739af16952883abce536958ac4877698277.zip | |
Fix compilation with new CompCert version
Diffstat (limited to 'src')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 5d9d578..3fab464 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -183,30 +183,30 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _) | Pand p1 p2 => match trans_pred n p1, trans_pred n p2 with - | Some (exist p1' _), Some (exist p2' _) => + | Some (exist _ p1' _), Some (exist _ p2' _) => Some (exist _ (p1' ++ p2') _) | _, _ => None end | Por p1 p2 => match trans_pred n p1, trans_pred n p2 with - | Some (exist p1' _), Some (exist p2' _) => + | Some (exist _ p1' _), Some (exist _ p2' _) => Some (exist _ (mult p1' p2') _) | _, _ => None end | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) | Pnot (Pnot p') => match trans_pred n p' with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end | Pnot (Pand p1 p2) => match trans_pred n (Por (Pnot p1) (Pnot p2)) with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end | Pnot (Por p1 p2) => match trans_pred n (Pand (Pnot p1) (Pnot p2)) with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end end @@ -239,9 +239,9 @@ Definition sat_pred (bound: nat) (p: pred_op) : + {forall a : asgn, sat_predicate p a = false}). refine ( match trans_pred bound p with - | Some (exist fm _) => + | Some (exist _ fm _) => match boundedSat bound fm with - | Some (inleft (exist a _)) => Some (inleft (exist _ a _)) + | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _)) | Some (inright _) => Some (inright _) | None => None end @@ -255,7 +255,7 @@ Qed. Definition sat_pred_simple (bound: nat) (p: pred_op) := match sat_pred bound p with - | Some (inleft (exist al _)) => Some (Some al) + | Some (inleft (exist _ al _)) => Some (Some al) | Some (inright _) => Some None | None => None end. |