diff options
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 40db4e45..3fd86728 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -86,7 +86,7 @@ Global Opaque builtin_res_eq_pos. Definition verify_match_inst dupmap inst tinst := match inst with - | Inop n => match tinst with Inop n' => do u <- verify_is_copy dupmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end + | Inop n => match tinst with Inop n' => verify_is_copy dupmap n n' | _ => Error(msg "verify_match_inst Inop") end | Iop op lr r n => match tinst with Iop op' lr' r' n' => @@ -167,10 +167,10 @@ Definition verify_match_inst dupmap inst tinst := if (list_eq_dec Pos.eq_dec lr lr') then if (eq_condition cond cond') then do u1 <- verify_is_copy dupmap n1 n1'; - do u2 <- verify_is_copy dupmap n2 n2'; OK tt + verify_is_copy dupmap n2 n2' else if (eq_condition (negate_condition cond) cond') then do u1 <- verify_is_copy dupmap n1 n2'; - do u2 <- verify_is_copy dupmap n2 n1'; OK tt + verify_is_copy dupmap n2 n1' else Error (msg "Incompatible conditions in Icond") else Error (msg "Different lr in Icond") | _ => Error (msg "verify_match_inst Icond") end @@ -212,7 +212,7 @@ Definition verify_mapping_match_nodes dupmap (f f': function): res unit := (** Verifies that the [dupmap] of the translated function [f'] is giving correct information in regards to [f] *) Definition verify_mapping dupmap (f f': function) : res unit := do u <- verify_mapping_entrypoint dupmap f f'; - do v <- verify_mapping_match_nodes dupmap f f'; OK tt. + verify_mapping_match_nodes dupmap f f'. (** * Entry points *) |