summaryrefslogtreecommitdiff
path: root/compiler/Config.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Config.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 98a5eea1..0abe94a9 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -3,9 +3,9 @@
(** {1 Backend choice} *)
(** The choice of backend *)
-type backend = FStar | Coq | Lean | HOL4
+type backend = FStar | Coq | Lean | HOL4 | IsabelleHOL
-let backend_names = [ "fstar"; "coq"; "lean"; "hol4" ]
+let backend_names = [ "fstar"; "coq"; "lean"; "hol4"; "IsabelleHOL"]
(** Utility to compute the backend from an input parameter *)
let backend_of_string (b : string) : backend option =
@@ -14,6 +14,7 @@ let backend_of_string (b : string) : backend option =
| "coq" -> Some Coq
| "lean" -> Some Lean
| "hol4" -> Some HOL4
+ | "IsabelleHOL" -> Some IsabelleHOL
| _ -> None
let opt_backend : backend option ref = ref None
@@ -374,7 +375,7 @@ let variant_concatenate_type_name = ref true
let use_tuple_structs = ref true
let backend_has_tuple_projectors backend =
- match backend with Lean -> true | Coq | FStar | HOL4 -> false
+ match backend with Lean -> true | Coq | FStar | HOL4 | IsabelleHOL -> false
(** Toggle the use of tuple projectors *)
let use_tuple_projectors = ref false