diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-18 17:30:09 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-21 19:36:38 +0100 |
commit | 589130e87d68227d25800e7506666eaf1d47a25a (patch) | |
tree | ff7ae021ca3c3306bbcbc8b9575b3b23b78320ce /interp/constrarg.mli | |
parent | 329b5b9ed526d572d7df066dc99486e1dcb9e4cc (diff) |
Changing the toplevel type of the int_or_var generic type to int.
Diffstat (limited to 'interp/constrarg.mli')
-rw-r--r-- | interp/constrarg.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrarg.mli b/interp/constrarg.mli index ef1ef4aee..f2f314eea 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -26,7 +26,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t (** {5 Additional generic arguments} *) -val wit_int_or_var : int or_var uniform_genarg_type +val wit_int_or_var : (int or_var, int or_var, int) genarg_type val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type |