From 8b1c09e551c02f26c524922570341f0f7fc78e2e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 10 Dec 2018 21:07:45 +0100
Subject: [coq] Adapt to coq/coq#9172

Note that this highlights some issues with the current Coq interface,
not clear what should we do.
---
 src/tac2core.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/tac2core.ml')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index aad4814744..8e92e154ac 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1142,7 +1142,8 @@ let () =
   let interp ist env sigma concl tac =
     let ist = Tac2interp.get_env ist in
     let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
-    let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in
+    let name, poly = Id.of_string "ltac2", false in
+    let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma concl tac in
     (EConstr.of_constr c, sigma)
   in
   GlobEnv.register_constr_interp0 wit_ltac2 interp
-- 
cgit v1.2.3