From f18502f32fb25b29cafe26340edbbcedd463c646 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 30 Oct 2017 11:40:49 +0100
Subject: Fix compilation after merge of Ltac_pretype interface.

---
 src/tac2core.ml    | 2 +-
 src/tac2interp.mli | 4 ++--
 src/tac2match.ml   | 2 +-
 src/tac2match.mli  | 2 +-
 src/tac2tactics.ml | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 1cfb34c249..9ef88a7d56 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -828,7 +828,7 @@ let open_constr_no_classes_flags () =
 let to_lvar ist =
   let open Glob_ops in
   let lfun = Tac2interp.set_env ist Id.Map.empty in
-  { empty_lvar with Glob_term.ltac_genargs = lfun }
+  { empty_lvar with Ltac_pretype.ltac_genargs = lfun }
 
 let gtypref kn = GTypRef (Other kn, [])
 
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index 211ac95196..21fdcd03af 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -20,8 +20,8 @@ val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
 
 (** {5 Cross-boundary encodings} *)
 
-val get_env : Glob_term.unbound_ltac_var_map -> environment
-val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound_ltac_var_map
+val get_env : Ltac_pretype.unbound_ltac_var_map -> environment
+val set_env : environment -> Ltac_pretype.unbound_ltac_var_map -> Ltac_pretype.unbound_ltac_var_map
 
 (** {5 Exceptions} *)
 
diff --git a/src/tac2match.ml b/src/tac2match.ml
index 7a22e91b6b..fef5647725 100644
--- a/src/tac2match.ml
+++ b/src/tac2match.ml
@@ -14,7 +14,7 @@ module NamedDecl = Context.Named.Declaration
 type context = EConstr.t
 
 type result = {
-  subst : Pattern.patvar_map ;
+  subst : Ltac_pretype.patvar_map ;
 }
 
 type match_pattern =
diff --git a/src/tac2match.mli b/src/tac2match.mli
index cf64542f40..7cfa1ed25f 100644
--- a/src/tac2match.mli
+++ b/src/tac2match.mli
@@ -30,4 +30,4 @@ val match_goal:
   match_rule ->
     ((Id.t * context option) list * (** List of hypotheses matching: name + context *)
     context option * (** Context for conclusion *)
-    Pattern.patvar_map (** Pattern variable substitution *)) Proofview.tactic
+    Ltac_pretype.patvar_map (** Pattern variable substitution *)) Proofview.tactic
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index b496f5046f..c68fdf9a7a 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -343,7 +343,7 @@ let discriminate ev arg =
 let injection ev ipat arg =
   let arg = Option.map (fun arg -> None, arg) arg in
   let ipat = Option.map mk_intro_patterns ipat in
-  let tac ev arg = Equality.injClause ipat ev arg in
+  let tac ev arg = Equality.injClause None ipat ev arg in
   on_destruction_arg tac ev arg
 
 let autorewrite ~all by ids cl =
-- 
cgit v1.2.3