diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Config.ml | 7 |
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 |