From 3addff470c8faeb6876c63575184caa0aa829e28 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 21 Jan 2021 22:18:50 +0000 Subject: Fix imports in Coq modules --- src/hls/Array.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'src/hls/Array.v') diff --git a/src/hls/Array.v b/src/hls/Array.v index 5c7ebc7..dec1335 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -18,9 +18,11 @@ Set Implicit Arguments. -Require Import Lia. -Require Import Vericertlib. -From Coq Require Import Lists.List Datatypes. +Require Import Coq.Init.Datatypes. +Require Import Coq.Lists.List. +Require Import Coq.micromega.Lia. + +Require Import vericert.common.Vericertlib. Import ListNotations. @@ -74,7 +76,7 @@ Lemma array_set_wf {A : Type} : Proof. induction l; intros; destruct i; auto. - invert H; crush; auto. + invert H; crush. Qed. Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := -- cgit