aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun_common.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun_common.mli')
-rw-r--r--plugins/funind/indfun_common.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index d802ecf2b..e0076735a 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -35,11 +35,11 @@ val list_union_eq :
val list_add_set_eq :
('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
-val chop_rlambda_n : int -> Rawterm.glob_constr ->
- (name*Rawterm.glob_constr*bool) list * Rawterm.glob_constr
+val chop_rlambda_n : int -> Glob_term.glob_constr ->
+ (name*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
-val chop_rprod_n : int -> Rawterm.glob_constr ->
- (name*Rawterm.glob_constr) list * Rawterm.glob_constr
+val chop_rprod_n : int -> Glob_term.glob_constr ->
+ (name*Glob_term.glob_constr) list * Glob_term.glob_constr
val def_of_const : Term.constr -> Term.constr
val eq : Term.constr Lazy.t