diff --git a/coq/args.ml b/coq/args.ml
index d9d5a56a..94bc48ba 100644
--- a/coq/args.ml
+++ b/coq/args.ml
@@ -90,7 +90,7 @@ let int_backend =
   in
   Arg.(
     value
-    & opt (enum [ ("Coq", Some Limits.Coq); ("Mp", Some Limits.Mp) ]) None
+    & opt (enum [ ("Coq", Some Limits.Coq); ("Mp", Some Limits.Mp); ("auto", None) ]) None
     & info [ "int_backend" ] ~docv:"INT_BACKEND" ~doc)
 
 let roots : string list Term.t =