From 620ffcb51f4f73b29ffe12366309e06cf906ef36 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 13 Apr 2011 14:27:29 +0000
Subject: Unify meta types with the right flags, add betaiotazeta reduction to
 unification (potentially harmful)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13991 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/R_sqr.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index eddf1dd04f..f23b9f178e 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -70,7 +70,7 @@ Proof.
   rewrite Rinv_mult_distr.
   repeat rewrite Rmult_assoc.
   apply Rmult_eq_compat_l.
-  pattern x at 2 in |- *; rewrite Rmult_comm.
+  rewrite Rmult_comm. 
   repeat rewrite Rmult_assoc.
   apply Rmult_eq_compat_l.
   reflexivity.
-- 
cgit v1.2.3