aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-04-18 14:39:34 +0200
committerPierre-Marie Pédrot2016-05-04 13:47:12 +0200
commitde4b9b68445d9f3e48da789404cbdfcd89214585 (patch)
treeaa383a63227fd77df70b8cc5c374ca7f08334ccf /pretyping/pretyping.ml
parentd2f0db714bd2d393423cf2dcb4ed37913029e052 (diff)
Moving the Val module to Geninterp.
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 5e6a3eac73..21eb100b4e 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;