From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/Registers.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Registers.v') diff --git a/backend/Registers.v b/backend/Registers.v index 20532e8c..cfe8427b 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -81,7 +81,7 @@ Lemma set_reg_lessdef: forall r v1 v2 rs1 rs2, Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2). Proof. - intros; red; intros. repeat rewrite Regmap.gsspec. + intros; red; intros. repeat rewrite Regmap.gsspec. destruct (peq r0 r); auto. Qed. -- cgit