Merge pull request #62 from proux01/micromega-core

Adapt to math-comp/math-comp#1448

Author: pi8027

theories/ssrZ.v

@@ -1,3 +1,4 @@
+From mathcomp Require all_algebra. (* remove this line when requiring Rocq > 9.1 *)
 From Coq Require Import ZArith.
 
 From HB Require Import structures.

theories/zify_algebra.v

@@ -1,3 +1,4 @@
+From mathcomp Require all_algebra. (* remove this line when requiring Rocq > 9.1 *)
 From Coq Require Import ZArith ZifyClasses ZifyBool.
 From Coq Require Export Lia.
 

theories/zify_ssreflect.v

@@ -1,3 +1,4 @@
+From mathcomp Require all_algebra. (* remove this line when requiring Rocq > 9.1 *)
 From Coq Require Import ZArith ZifyClasses ZifyInst ZifyBool.
 From Coq Require Export Lia.
 From Coq Require Znumtheory.