Skip to content

Commit 1d07e86

Browse files
committed
boot
1 parent 1dc2382 commit 1d07e86

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

repeatxy.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
From HB Require Import structures.
2-
From mathcomp Require Import all_ssreflect.
2+
From mathcomp Require Import all_boot.
33
From Stdlib Require Import NArith.
44
Require Import digitn.
55

0 commit comments

Comments
 (0)