Skip to content

Commit

Permalink
fixing build
Browse files Browse the repository at this point in the history
  • Loading branch information
zstone1 committed Oct 4, 2024
1 parent 6d98837 commit 9714276
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 1 deletion.
1 change: 1 addition & 0 deletions theories/Make
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ reals.v
landau.v
Rstruct.v
topology.v
separation_axioms.v
function_spaces.v
cantor.v
prodnormedzmodule.v
Expand Down
1 change: 0 additions & 1 deletion theories/function_spaces.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import cardinality mathcomp_extra fsbigop.

From mathcomp Require Import reals signed topology separation_axioms.

(**md**************************************************************************)
Expand Down

0 comments on commit 9714276

Please sign in to comment.