diff options
Diffstat (limited to 'interp/implicit_quantifiers.mli')
| -rw-r--r-- | interp/implicit_quantifiers.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 0d28eccad..8f02eb765 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -24,6 +24,8 @@ open Libnames open Typeclasses (*i*) +val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit + val ids_of_list : identifier list -> Idset.t val destClassApp : constr_expr -> loc * reference * constr_expr list val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list |