From 782372856e836ca106011fada44695c224ae572d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 10 Feb 2010 13:43:19 +0000
Subject: Euclidean division for NArith

 There was already a Ndiv and Nmod, but hiddent in ZOdiv_def. We
 higlight it by putting it in a separate file, prove its specification
 without using Z (but for the moment can't avoid a detour via nat,
 though), and then instantiate general results from Natural/Abstract/NDiv

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

(limited to 'plugins')

diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index b5384f80b4..1bbdf51515 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -13,7 +13,7 @@ Require Import BinNat.
 Require Import Setoid.
 Require Import Ring_theory.
 Require Import Ring_polynom.
-Require Import ZOdiv_def.
+Require Import Ndiv_def ZOdiv_def.
 Import List.
 
 Set Implicit Arguments.
-- 
cgit v1.2.3