Merge pull request coq/ltac2#92 from ejgallego/proofview+proof_info

[coq] Adapt to coq/coq#9173

2 files changed, 3 insertions, 1 deletions

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 =