diff options
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/library/impargs.mli b/library/impargs.mli index de8d89166..4fb056986 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -143,3 +143,5 @@ type implicit_discharge_request = | ImplInteractive of global_reference * implicits_flags * implicit_interactive_request +val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool +(** Equality on [explicitation]. *) |