Commit 6ced6d63 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Silly bug.

parent 206abba6
Pipeline #65231 passed with stages
in 21 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
from_menhirlib f; fprintf f "Require Version.\n";
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