lltodk: use signature_name.conjecture

Author: fblanqui

.github/workflows/main.yml

@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.1, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
+        ocaml-version: [5.4.1, 5.3.0, 5.2.1, 4.14.2] #5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
     runs-on: ubuntu-latest
     steps:
       - name: checking out lambdapi repo ...

lltodk.ml

@@ -1061,15 +1061,17 @@ let output_term oc phrases _ llp =
   let goal_name = (List.hd llp).name in
   let dkproof = make_proof_term (List.hd goal) prooftree in
   fprintf oc "#REQUIRE zenon.\n";
-  if !Globals.signature_name <> "" then
+  let sig_name = !Globals.signature_name in
+  if sig_name <> "" then
     begin
       fprintf oc "#REQUIRE %s.\n" !Globals.signature_name;
       fprintf oc "\n[] %s.%s --> " !Globals.signature_name goal_name
     end
   else fprintf oc "\n[] %s --> " goal_name;
   if !Globals.conjecture <> "" then
     fprintf oc "__negated_conjecture_proof__ : \
-                zenon.proof (zenon.not Signature.conjecture) =>\n";
+                zenon.proof (zenon.not %sconjecture) =>\n"
+      (if sig_name <> "" then sig_name^"." else "")
   fprintf oc "zenon.nnpp (%a)\n(%a)"
     print_dk_term dkgoal print_dk_term dkproof;
   if !Globals.signature_name <> "" then fprintf oc ".";