Skip to content

require Arith and use RelationClasses (for stdlib#150 and stdlib#152) #821

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
andres-erbsen wants to merge 1 commit into from
Closed

require Arith and use RelationClasses (for stdlib#150 and stdlib#152) #821

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions msl/subtypes.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,11 @@
*
*)

Require Import Arith.
Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.predicates_hered.

Import Arith.

Local Open Scope pred.

Section Fash.
Expand Down
5 changes: 3 additions & 2 deletions zlist/list_solver.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
Require Import RelationClasses.
Require Import ZArith Znumtheory.
Require Import Coq.Lists.List.
Require Import Lia.
Expand Down Expand Up @@ -1030,8 +1031,8 @@ Section Sorted.
Variable A : Type.
Variable d : Inhabitant A.
Variable le : A -> A -> Prop.
Context {Hrefl : Relations_1.Reflexive A le}.
Context {Htrans : Relations_1.Transitive le}.
Context {Hrefl : Reflexive le}.
Context {Htrans : Transitive le}.

Definition sorted (l : list A) :=
forall i j, 0 <= i <= j /\ j < Zlength l -> le (Znth i l) (Znth j l).
Expand Down
Loading