Do not require all_ssreflect

jasmin-lang · May 23, 2024 · 4121a52 · 4121a52
1 parent 00c2a20
commit 4121a52
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/src/word.v b/src/word.v
@@ -22,7 +22,8 @@
 
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint intdiv zmodp.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice div fintype tuple bigop prime order.
+From mathcomp Require Import ssralg ssrnum ssrint intdiv zmodp.
 From Coq Require Import Arith ZArith Lia.
 Require Import word_ssrZ.
 

diff --git a/src/word_ssrZ.v b/src/word_ssrZ.v
@@ -22,7 +22,8 @@
 
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint intdiv.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat div bigop choice order.
+From mathcomp Require Import ssralg ssrnum ssrint intdiv.
 From Coq Require Import Arith ZArith.
 
 Set Implicit Arguments.