Merge pull request #117 from proux01/stdlib_repo

Adapt to coq/coq#19530
mit-pdos · Sep 17, 2024 · d4f705d · d4f705d
2 parents 9ae5f9c + 4586708
commit d4f705d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Helpers/LittleEndian.v b/src/Helpers/LittleEndian.v
@@ -2,7 +2,7 @@
 
 https://github.com/mit-plv/coqutil/blob/f3209a5b2c22eb36c3c1a8688b2a18b0d40fd476/src/coqutil/Word/LittleEndian.v
  *)
-From Coq Require Import ZArith.ZArith.
+From Coq Require Import ZArith.
 From coqutil Require Import Z.Lia.
 From coqutil Require Import Word.Interface Datatypes.HList Datatypes.PrimitivePair.
 From coqutil Require Import Word.Properties.

diff --git a/src/goose_lang/lang.v b/src/goose_lang/lang.v
@@ -1,4 +1,4 @@
-From Coq Require Import Program.Equality.
+From Coq.Program Require Import Equality.
 From RecordUpdate Require Import RecordSet.
 From stdpp Require Export binders strings.
 From stdpp Require Import gmap.