Skip to content

GitLab

why3
why3
Commit 1f3e60bb authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

minor housekeeping in src/printers/

parent b706aaf0
Hide whitespace changes
Inline Side-by-side
Showing with 102 additions and 3 deletions
Makefile.in
View file @ 1f3e60bb
......@@ -133,7 +133,8 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
introduction abstraction close_epsilon lift_epsilon \
eval_match
LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa cvc3
LIB_PRINTER = print_real alt_ergo why3printer smtv1 smtv2 \
coq tptp simplify gappa cvc3
LIBMODULES = src/config \
$(addprefix src/util/, $(LIB_UTIL)) \
......
src/main.ml
View file @ 1f3e60bb
......@@ -498,7 +498,7 @@ let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_glist) =
in
let ch = open_out oldf in
let fmt = formatter_of_out_channel ch in
Coq.print_theory ~old env [] Ident.Mid.empty fmt th
Coq.print_theory ?old env [] Ident.Mid.empty fmt th
let do_input env drv = function
| None, _ when !opt_parse_only || !opt_type_only ->
......
src/printer/coq.ml
View file @ 1f3e60bb
......@@ -547,7 +547,7 @@ let print_tdecl ~old info fmt d = match d.td_node with
let print_tdecls ~old info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_tdecl ~old info)) dl
let print_theory _env pr thpr ~old fmt th =
let print_theory _env pr thpr ?old fmt th =
forget_all ();
print_prelude fmt pr;
print_prelude_for_theory th fmt thpr;
......
src/printer/coq.mli 0 → 100644
View file @ 1f3e60bb
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
val print_theory : Env.env -> Printer.prelude -> Printer.prelude_map ->
?old:Pervasives.in_channel -> Format.formatter -> Theory.theory -> unit
src/printer/gappa.mli 0 → 100644
View file @ 1f3e60bb
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
src/printer/smtv1.mli 0 → 100644
View file @ 1f3e60bb
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
src/printer/smtv2.mli 0 → 100644
View file @ 1f3e60bb
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
src/printer/why3printer.mli 0 → 100644
View file @ 1f3e60bb
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
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