diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 9169e5fbf1..1554d42898 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -141,8 +141,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr (* Interprets into a abbreviatable constr *) -val interp_aconstr : implicits_env -> identifier list -> constr_expr -> - interpretation +val interp_aconstr : implicits_env -> identifier list * identifier list + -> constr_expr -> interpretation (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b |