Correct behaviour for -gdv (#52)

* Correct behaviour for the -gdv flag

Author: gburel

lltolp.ml

@@ -1059,12 +1059,13 @@ let output_term oc phrases _ llp =
   let prooftree = extract_prooftree llp in
   let goal_name = (List.hd llp).name in
   let dkproof = make_proof_term (List.hd goal) prooftree in
-  fprintf oc "require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL \
-              Logic.Zenon.Main;\n";
   if !Globals.gdv then
     fprintf oc "\nrule F.%s ↪ " goal_name
-  else
-    fprintf oc "\nsymbol %s ≔ " goal_name;
+  else begin
+      fprintf oc "require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL \
+                  Logic.Zenon.Main;\n";
+      fprintf oc "\nsymbol %s ≔ " goal_name
+    end;
   if !Globals.conjecture <> "" then
     fprintf oc "λ __negated_conjecture_proof__,";
   begin

lpprint.ml

@@ -112,7 +112,7 @@ and print_dk_cst typ o (t, var_context) =
     if Mltoll.is_meta s then fprintf o "select (%a)" print_dk_zentype_aux (typ, var_context)
     else
        begin
-         fprintf o (if !Globals.gdv then "%s"
+         fprintf o (if not !Globals.gdv then "%s"
                     else if is_formula then "F.%s"
                     else "S.%s")
            (escape_name s);