diff options
Diffstat (limited to 'driver/main_args.mli')
| -rw-r--r-- | driver/main_args.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/main_args.mli b/driver/main_args.mli index 27fb475ae0..c45fd076d2 100644 --- a/driver/main_args.mli +++ b/driver/main_args.mli @@ -203,6 +203,7 @@ module type Optcommon_options = sig val _dflambda_verbose : unit -> unit val _drawclambda : unit -> unit val _dclambda : unit -> unit + val _dcmm_invariants : unit -> unit val _dcmm : unit -> unit val _dsel : unit -> unit val _dcombine : unit -> unit |