Commit d0593e9a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Sillier bug.

parent 6ced6d63
Pipeline #65232 passed with stages
in 20 seconds
......@@ -515,7 +515,7 @@ module Run (T: sig end) = struct
fprintf f "From Coq.Numbers Require Import BinNums.\n";
from_menhirlib f; fprintf f "Require Main.\n";
if not Settings.coq_no_version_check then
begin from_menhirlib f; fprintf f "Require Version.\n" end
begin from_menhirlib f; fprintf f "Require Version.\n" end;
fprintf f "Import List.ListNotations.\n\n";
if not Settings.coq_no_version_check then
......
Markdown is supported
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