From fc3c1660ee62b5341ccf75505aa63dca0d2cf16c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 9 Mar 2020 21:58:53 +0100
Subject: get moves

---
 backend/CSE3analysis.v | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index f0af0ac7..da527995 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -119,21 +119,12 @@ Proof.
   - right; congruence.
 Qed.
 
-Definition get_move (eq : equation) :=
-  if is_smove (eq_op eq)
-  then match eq_args eq with
-       | h::nil => Some h
-       | _ => None
-       end
-  else None.
-
 Definition get_moves (eqs : PTree.t equation) :
   Regmap.t PSet.t :=
   PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
-                match get_move eq with
-                | Some rhs => add_i_j (eq_lhs eq) rhs already
-                | None => already
-                end) eqs (PMap.init PSet.empty).
+                if is_smove (eq_op eq)
+                then add_i_j (eq_lhs eq) eqno already
+                else already) eqs (PMap.init PSet.empty).
 
 Record eq_context := mkeqcontext
                        { eq_catalog : node -> option equation;
-- 
cgit