Skip to content

Commit

Permalink
import -> export Extr* in ExtractAlgorithm.v
Browse files Browse the repository at this point in the history
  • Loading branch information
palmskog committed Jan 12, 2022
1 parent b0d92aa commit bef9e05
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions coq/Algorithms/ExtractAlgorithm.v
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
From Coq Require Import Arith NPeano.
(* Require Import PeanoNat. *)
From Coq Require Import List Ascii String.
(* TODO: double check that this gets used *)
From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlString.
From Coq Require Export ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlString.

Extract Inlined Constant length => "List.length".
Extract Inlined Constant negb => "not".
Expand Down

0 comments on commit bef9e05

Please sign in to comment.