Skip to content

Commit

Permalink
fixing build broken by changed dependency
Browse files Browse the repository at this point in the history
  • Loading branch information
vzaliva committed Aug 29, 2023
1 parent 0ed72b0 commit f84f9ea
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion coq/extracted/Extract.v
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,6 @@ Extract Constant ClassicalDedekindReals.sig_not_dec => false. (* Ugh *)

(* Set Extraction AccessOpaque. *)

Extraction Library Vector.
(* Extraction Library Vector. *)
Recursive Extraction Library MorelloCapsGS.
Recursive Extraction Library CheriMemory.

0 comments on commit f84f9ea

Please sign in to comment.