From 67cff8c545a25e7fa1a29b08d41fc64a7278508b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 17 Dec 2018 19:01:04 +0100
Subject: [coq] Adapt to coq/coq#9137

To be merged when the upstream PR is merged.

Not sure this is the right thing to do tho.
---
 src/dune           | 1 +
 src/tac2tactics.ml | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/dune b/src/dune
index 7c911fb041..4a018adb9a 100644
--- a/src/dune
+++ b/src/dune
@@ -2,6 +2,7 @@
  (name ltac2)
  (public_name coq.plugins.ltac2)
  (modules_without_implementation tac2expr tac2qexpr tac2types)
+ (flags :standard -w -50)
  (libraries coq.plugins.firstorder))
 
 (rule
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index bc92ab43a8..059a1babd7 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -29,7 +29,8 @@ let tactic_infer_flags with_evar = {
 (** FIXME: export a better interface in Tactics *)
 let delayed_of_tactic tac env sigma =
   let _, pv = Proofview.init sigma [] in
-  let c, pv, _, _ = Proofview.apply env tac pv in
+  let name, poly = Id.of_string "ltac2_delayed", false in
+  let c, pv, _, _ = Proofview.apply ~name ~poly env tac pv in
   (sigma, c)
 
 let delayed_of_thunk r tac env sigma =
-- 
cgit v1.2.3