diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 99e7d68bbc..b135caf505 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -93,3 +93,7 @@ val interp_aconstr : identifier list -> constr_expr -> interpretation (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b + +(* For v8 translation *) +val set_temporary_implicits_in : + (identifier * Impargs.implicits_list) list -> unit |