add renamings for coq output (#124)

Deducteam · Apr 12, 2024 · 5442fc9 · 5442fc9
1 parent 598b944
commit 5442fc9
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/renaming.lp b/renaming.lp
@@ -76,8 +76,6 @@ builtin "mulmul" ≔ **;
 builtin "mulmul_def" ≔ **_def;
 builtin "ltle" ≔ <<=;
 builtin "ltle_def" ≔ <<=_def;
-builtin "mapsto" ≔ vdash>;
-builtin "mapsto_def" ≔ vdash>_def;
 
 // Multivariate
 builtin "add_c" ≔ +_c;
@@ -90,3 +88,5 @@ builtin "pow_c" ≔ ^_c;
 builtin "pow_c_def" ≔ ^_c_def;
 builtin "_at" ≔ at;
 builtin "_at_def" ≔ at_def;
+builtin "S'" ≔ S;
+builtin "pair'" ≔ pair;
diff --git a/xlp.ml b/xlp.ml
@@ -17,6 +17,7 @@ let name =
     [ "|----", "vdash4"
     ; "|---", "vdash3"
     ; "|--", "vdash2"
+    ; "|->", "mapsto"
     ; "|-", "vdash"
     ; "|=>", "bar_imp"]
   in
@@ -50,7 +51,6 @@ let name =
     |"sequential"|"simplify"|"solve"|"symbol"|"symmetry"|"type"|"TYPE"
     |"unif_rule"|"verbose"|"why3"|"with" -> "_" ^ n
     (* for Coq *)
-    | "S" -> "S'"
     | "%" -> n
     | _ -> Xlib.change_prefixes prefixes (Xlib.replace '%' '_' n)
     end