summaryrefslogtreecommitdiff
path: root/compiler/Config.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Config.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index cc80e452..1c3d14ff 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -3,13 +3,13 @@
(** {1 Backend choice} *)
(** The choice of backend *)
-type backend = FStar | Coq
+type backend = FStar | Coq | Lean
-let backend_names = [ "fstar"; "coq" ]
+let backend_names = [ "fstar"; "coq"; "lean" ]
(** Utility to compute the backend from an input parameter *)
let backend_of_string (b : string) : backend option =
- match b with "fstar" -> Some FStar | "coq" -> Some Coq | _ -> None
+ match b with "fstar" -> Some FStar | "coq" -> Some Coq | "lean" -> Some Lean | _ -> None
let opt_backend : backend option ref = ref None