summaryrefslogtreecommitdiff
path: root/plugins/ltac/tacsubst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tacsubst.ml')
-rw-r--r--plugins/ltac/tacsubst.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index a1d8b087..4626378d 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,8 @@ open Mod_subst
open Genarg
open Stdarg
open Tacarg
-open Misctypes
+open Tactypes
+open Tactics
open Globnames
open Genredexpr
open Patternops
@@ -75,7 +76,7 @@ let subst_and_short_name f (c,n) =
(* assert (n=None); *)(* since tacdef are strictly globalized *)
(f c,None)
-let subst_or_var f = function
+let subst_or_var f = let open Locus in function
| ArgVar _ as x -> x
| ArgArg x -> ArgArg (f x)
@@ -112,7 +113,7 @@ let subst_glob_constr_or_pattern subst (bvars,c,p) =
(bvars,subst_glob_constr subst c,subst_pattern subst p)
let subst_redexp subst =
- Miscops.map_red_expr_gen
+ Redops.map_red_expr_gen
(subst_glob_constr subst)
(subst_evaluable subst)
(subst_glob_constr_or_pattern subst)