Commit b1f7d829 authored by Francois Bobot's avatar Francois Bobot
Browse files

smt : Ajout du nom de l'axiom en commentaire

parent 6f082459
......@@ -177,8 +177,9 @@ let print_decl drv fmt d = match d.d_node with
| Dind _ -> unsupportedDecl d
"smt : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name -> false
| Dprop (Paxiom, _pr, f) ->
fprintf fmt "@[<hov 2>:assumption@ %a@]@\n"
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>;; %s@\n:assumption@ %a@]@\n"
pr.pr_name.id_string
(print_fmla drv) f; true
| Dprop (Pgoal, pr, f) ->
fprintf fmt "@[:formula@\n";
......
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