diff options
Diffstat (limited to 'compiler/Config.ml')
| -rw-r--r-- | compiler/Config.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 15818938..ce9b0e0c 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 +type backend = FStar | Coq | Lean | HOL4 -let backend_names = [ "fstar"; "coq"; "lean" ] +let backend_names = [ "fstar"; "coq"; "lean"; "hol4" ] (** Utility to compute the backend from an input parameter *) let backend_of_string (b : string) : backend option = @@ -13,6 +13,7 @@ let backend_of_string (b : string) : backend option = | "fstar" -> Some FStar | "coq" -> Some Coq | "lean" -> Some Lean + | "hol4" -> Some HOL4 | _ -> None let opt_backend : backend option ref = ref None |