From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 theories/QArith/Qcanon.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'theories/QArith/Qcanon.v')

diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index a865a6cf..f7f83bf0 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -70,7 +70,6 @@ Qed.
 
 Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q).
 Arguments Q2Qc q%Q.
-Notation " !! " := Q2Qc : Qc_scope.
 
 Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
 Proof.
@@ -87,8 +86,8 @@ Proof.
 Qed.
 Hint Resolve Qc_is_canon.
 
-Notation " 0 " := (!!0) : Qc_scope.
-Notation " 1 " := (!!1) : Qc_scope.
+Notation " 0 " := (Q2Qc 0) : Qc_scope.
+Notation " 1 " := (Q2Qc 1) : Qc_scope.
 
 Definition Qcle (x y : Qc) := (x <= y)%Q.
 Definition Qclt (x y : Qc) := (x < y)%Q.
@@ -144,15 +143,15 @@ Defined.
 (** The addition, multiplication and opposite are defined
    in the straightforward way: *)
 
-Definition Qcplus (x y : Qc) := !!(x+y).
+Definition Qcplus (x y : Qc) := Q2Qc (x+y).
 Infix "+" := Qcplus : Qc_scope.
-Definition Qcmult (x y : Qc) := !!(x*y).
+Definition Qcmult (x y : Qc) := Q2Qc (x*y).
 Infix "*" := Qcmult : Qc_scope.
-Definition Qcopp (x : Qc) := !!(-x).
+Definition Qcopp (x : Qc) := Q2Qc (-x).
 Notation "- x" := (Qcopp x) : Qc_scope.
 Definition Qcminus (x y : Qc) := x+-y.
 Infix "-" := Qcminus : Qc_scope.
-Definition Qcinv (x : Qc) := !!(/x).
+Definition Qcinv (x : Qc) := Q2Qc (/x).
 Notation "/ x" := (Qcinv x) : Qc_scope.
 Definition Qcdiv (x y : Qc) := x*/y.
 Infix "/" := Qcdiv : Qc_scope.
@@ -434,14 +433,14 @@ Qed.
 Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 <  z  -> x*z <= y*z -> x <= y.
 Proof.
   unfold Qcmult, Qcle, Qclt; intros; simpl in *.
-  repeat progress rewrite Qred_correct in * |-.
+  rewrite !Qred_correct in * |-.
   eapply Qmult_lt_0_le_reg_r; eauto.
 Qed.
 
 Lemma Qcmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.
 Proof.
   unfold Qcmult, Qclt; intros; simpl in *.
-  repeat progress rewrite Qred_correct in *.
+  rewrite !Qred_correct in *.
   eapply Qmult_lt_compat_r; eauto.
 Qed.
 
@@ -460,13 +459,13 @@ Proof.
   induction n; simpl; auto with qarith.
   rewrite IHn; auto with qarith.
 Qed.
-
+Transparent Qred.
 Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.
 Proof.
   destruct n; simpl.
   destruct 1; auto.
   intros.
-  now apply Qc_is_canon.
+  now apply Qc_is_canon. 
 Qed.
 
 Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n.
@@ -521,6 +520,7 @@ Add Field Qcfield : Qcft.
 (** A field tactic for rational numbers *)
 
 Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc.
+Proof.
 intros.
 field.
 auto.
-- 
cgit v1.2.3