From bccc54dc85e2d9cd7248c24a576d6092630fb51d Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Sat, 28 Jul 2018 21:30:02 +0200
Subject: moving countalg and closed_field around

- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style
---
 mathcomp/algebra/ssrint.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'mathcomp/algebra/ssrint.v')

diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index f12784b..d0214dd 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp
-Require Import fintype finfun bigop ssralg ssrnum poly.
+Require Import fintype finfun bigop ssralg countalg ssrnum poly.
 Import GRing.Theory Num.Theory.
 
 (******************************************************************************)
@@ -359,6 +359,13 @@ Canonical int_comUnitRing := Eval hnf in [comUnitRingType of int].
 Canonical int_iDomain :=
   Eval hnf in IdomainType int intUnitRing.idomain_axiomz.
 
+Canonical int_countZmodType := [countZmodType of int].
+Canonical int_countRingType := [countRingType of int].
+Canonical int_countComRingType := [countComRingType of int].
+Canonical int_countUnitRingType := [countUnitRingType of int].
+Canonical int_countComUnitRingType := [countComUnitRingType of int].
+Canonical int_countIdomainType := [countIdomainType of int].
+
 Definition absz m := match m with Posz p => p | Negz n => n.+1 end.
 Notation "m - n" :=
   (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
-- 
cgit v1.2.3