aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrarg.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-18 17:30:09 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-21 19:36:38 +0100
commit589130e87d68227d25800e7506666eaf1d47a25a (patch)
treeff7ae021ca3c3306bbcbc8b9575b3b23b78320ce /interp/constrarg.mli
parent329b5b9ed526d572d7df066dc99486e1dcb9e4cc (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.mli2
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