From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 plugins/ltac/tacsubst.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac/tacsubst.ml')

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)
-- 
cgit v1.2.3