Coq -> Stdlib

Author: pi8027

theories/ssrZ.v

@@ -1,4 +1,4 @@
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.

theories/zify.v

@@ -1,4 +1,4 @@
-From Coq Require Export Lia.
+From Stdlib Require Export Lia.
 From mathcomp Require Import zify_ssreflect zify_algebra.
 Export SsreflectZifyInstances.Exports.
 Export AlgebraZifyInstances.Exports.

theories/zify_algebra.v

@@ -1,5 +1,5 @@
-From Coq Require Import ZArith ZifyClasses ZifyBool.
-From Coq Require Export Lia.
+From Stdlib Require Import ZArith ZifyClasses ZifyBool.
+From Stdlib Require Export Lia.
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.

theories/zify_ssreflect.v

@@ -1,6 +1,6 @@
-From Coq Require Import ZArith ZifyClasses ZifyInst ZifyBool.
-From Coq Require Export Lia.
-From Coq Require Znumtheory.
+From Stdlib Require Import ZArith ZifyClasses ZifyInst ZifyBool.
+From Stdlib Require Export Lia.
+From Stdlib Require Znumtheory.
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.