From e3e6ff629e258269bc9fe06f7be99a2d5f334071 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 7 Jan 2010 15:32:46 +0000
Subject: Numbers: separation of funs, notations, axioms. Notations via module,
 without scope.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

(limited to 'theories/Numbers/Integer/SpecViaZ')

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index f752c19761..666ce5454f 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -16,18 +16,15 @@ Require Import ZSig.
 
 Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig.
 
-Delimit Scope NumScope with Num.
-Bind Scope NumScope with Z.t.
-Local Open Scope NumScope.
-Local Notation "[ x ]" := (Z.to_Z x) : NumScope.
-Local Infix "=="  := Z.eq (at level 70) : NumScope.
-Local Notation "0" := Z.zero : NumScope.
-Local Infix "+" := Z.add : NumScope.
-Local Infix "-" := Z.sub : NumScope.
-Local Infix "*" := Z.mul : NumScope.
-Local Notation "- x" := (Z.opp x) : NumScope.
-Local Infix "<=" := Z.le : NumScope.
-Local Infix "<" := Z.lt : NumScope.
+Local Notation "[ x ]" := (Z.to_Z x).
+Local Infix "=="  := Z.eq (at level 70).
+Local Notation "0" := Z.zero.
+Local Infix "+" := Z.add.
+Local Infix "-" := Z.sub.
+Local Infix "*" := Z.mul.
+Local Notation "- x" := (Z.opp x).
+Local Infix "<=" := Z.le.
+Local Infix "<" := Z.lt.
 
 Hint Rewrite
  Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ
-- 
cgit v1.2.3