Skip to content

Commit b4b1daa

Browse files
committed
1 parent 55c6e6d commit b4b1daa

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

extraction/extraction.v

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,8 @@ Require Initializers.
2727
(* Standard lib *)
2828
From Coq Require Import ExtrOcamlBasic ExtrOcamlNativeString.
2929

30+
Set Extraction OldCoqPrefix. (* TODO: handle when requiring Rocq >= 9.4 *)
31+
3032
(* Coqlib *)
3133
Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".
3234

0 commit comments

Comments
 (0)