diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-17 23:19:16 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-17 23:19:16 +0200 |
| commit | bf443e2f2bf38c30c9b68020c7c43cd7b3e10549 (patch) | |
| tree | 87696f4b78894ceb46d44b1d7e2aea9375865c5d /scheduling/BTL.v | |
| parent | ee558407e59c6794daad70aab2e1e7794535367e (diff) | |
| download | compcert-kvx-bf443e2f2bf38c30c9b68020c7c43cd7b3e10549.tar.gz compcert-kvx-bf443e2f2bf38c30c9b68020c7c43cd7b3e10549.zip | |
preparing compiler passes and ml oracles
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 10a000a8..9fdf39be 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -463,8 +463,8 @@ Local Open Scope error_monad_scope. Definition verify_is_copy dupmap n n' := match dupmap!n with - | None => Error(msg "verify_is_copy None") - | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + | None => Error(msg "BTL.verify_is_copy None") + | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.verify_is_copy invalid map") end end. Fixpoint verify_is_copy_list dupmap ln ln' := @@ -472,9 +472,9 @@ Fixpoint verify_is_copy_list dupmap ln ln' := | n::ln => match ln' with | n'::ln' => do _ <- verify_is_copy dupmap n n'; verify_is_copy_list dupmap ln ln' - | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end | nil => match ln' with - | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'") | nil => OK tt end end. |