aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/implicit_quantifiers.ml')
-rw-r--r--interp/implicit_quantifiers.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b430c000bf..428ddd6ab9 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -293,7 +293,7 @@ let implicit_application env ?(allow_partial=true) f ty =
CAppExpl (loc, (None, id), args), avoid
in c, avoid
-let implicits_of_rawterm ?(with_products=true) l =
+let implicits_of_glob_constr ?(with_products=true) l =
let rec aux i c =
let abs loc na bk t b =
let rest = aux (succ i) b in