diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 21:42:08 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 21:42:08 +0100 |
| commit | 12fad0dfecb626ceafcbb6e75c6adfd5e108b420 (patch) | |
| tree | 3d14ce842874c8de15d9cddc73b22b27410cd996 /backend/Duplicate.v | |
| parent | b8e73be77abdef268594e747bdc6fc1ba503dc1f (diff) | |
| download | compcert-kvx-12fad0dfecb626ceafcbb6e75c6adfd5e108b420.tar.gz compcert-kvx-12fad0dfecb626ceafcbb6e75c6adfd5e108b420.zip | |
remove some useless "OK tt"
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 *) |