From 66c523bcac8b64e202baa084bf24f5b57c61fcd6 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 6 Mar 2018 16:12:28 +0000 Subject: [stdlib] Do not use “Require” inside sections MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- plugins/nsatz/Nsatz.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/nsatz') diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 85e2a5b23..c5a09d677 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -30,6 +30,7 @@ Require Export Ncring_initial. Require Export Ncring_tac. Require Export Integral_domain. Require Import DiscrR. +Require Import ZArith. Declare ML Module "nsatz_plugin". @@ -56,9 +57,8 @@ simpl. simpl; cring. Qed. (* adpatation du code de Benjamin aux setoides *) -Require Import ZArith. -Require Export Ring_polynom. -Require Export InitialRing. +Export Ring_polynom. +Export InitialRing. Definition PolZ := Pol Z. Definition PEZ := PExpr Z. -- cgit v1.2.3