Commit 228fdc0a authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Coq back-end: add a few newlines in the generated file for readability.

parent ad65c43a
# Changes
## 2018/09/10
* Coq back-end: add a few newlines in the generated file for readability.
(Suggested by Bernhard Schommer.)
## 2018/09/05
* When `--explain` is enabled, always create a fresh `.conflicts` file
......
......@@ -124,14 +124,13 @@ module Run (T: sig end) = struct
fprintf f "Program Instance %sNum : Numbered %s :=\n" name name;
fprintf f " { inj := fun x => match x return _ with ";
iteri (fun k constr ->
fprintf f "| %s => " constr;
write_optimized_int31 f k;
fprintf f " ";
fprintf f "\n | %s => " constr;
write_optimized_int31 f k
);
fprintf f "end;\n";
fprintf f "\n end;\n";
fprintf f " surj := (fun n => match n return _ with ";
iteri (fprintf f "| %d => %s ");
fprintf f "| _ => %s end)%%int31;\n" (List.hd constrs);
iteri (fprintf f "\n | %d => %s ");
fprintf f "\n | _ => %s\n end)%%int31;\n" (List.hd constrs);
fprintf f " inj_bound := %d%%int31 }.\n" (List.length constrs);
end
else
......
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