aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5e6a3eac7..21eb100b4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -49,7 +49,7 @@ open Context.Named.Declaration
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
type var_map = constr_under_binders Id.Map.t
type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Genarg.Val.t Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
type ltac_var_map = {
ltac_constrs : var_map;
ltac_uconstrs : uconstr_var_map;