Skip to content
Snippets Groups Projects
Commit ba5e4a82 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build

parent dff135cd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 1 deletion
theories/sets.v
+ 2
− 1
View file @ ba5e4a82
...@@ -2,7 +2,8 @@ ...@@ -2,7 +2,8 @@
importantly, it implements some tactics to automatically solve goals involving importantly, it implements some tactics to automatically solve goals involving
sets. *) sets. *)
From stdpp Require Export orders list list_numbers. From stdpp Require Export orders list list_numbers.
From stdpp Require Import options finite. From stdpp Require Import finite.
From stdpp Require Import options.
(* FIXME: This file needs a 'Proof Using' hint, but they need to be set (* FIXME: This file needs a 'Proof Using' hint, but they need to be set
locally (or things moved out of sections) as no default works well enough. *) locally (or things moved out of sections) as no default works well enough. *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment