diff options
| author | Maxime Dénès | 2018-03-08 10:11:49 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-08 10:11:49 +0100 |
| commit | c31c6d92d2b2c314ea9c633f9e0f14500c2785b0 (patch) | |
| tree | 7cd0f3c56b5b1e6dbf433e66e1d03fbb89d1f8a8 /plugins/nsatz | |
| parent | c5cd6f93bc14c66a3e4d7e17f8d18dc9fb2308d7 (diff) | |
| parent | 5cbb460234e32f5e325c60aaada91d3cea298b9f (diff) | |
Merge PR #6934: Warn when using “Require” in a section
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 85e2a5b235..c5a09d677e 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. |