Commit 1d7ca028 authored by jjourdan's avatar jjourdan

Coq backend : Unset Elimination Schemes

git-svn-id: svn+ssh:// 0f8b5475-4b4e-0410-85a8-ee3154a6bfe7
parent 7551eba0
......@@ -480,6 +480,7 @@ module Run (T: sig end) = struct
fprintf f "Require Import Alphabet.\n";
fprintf f "Require Grammar.\n";
fprintf f "Require Automaton.\n\n";
fprintf f "Unset Elimination Schemes.\n\n";
write_grammar f;
write_automaton f;
write_theorems f;
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