aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-12-17 19:01:04 +0100
committerEmilio Jesus Gallego Arias2019-02-09 17:46:36 +0100
commit67cff8c545a25e7fa1a29b08d41fc64a7278508b (patch)
tree99f3a46374bdecb25f16bd1109f6d8e690071841
parent2216604fb42a4fe2013e25d95e0c6a5f715db287 (diff)
[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.
-rw-r--r--src/dune1
-rw-r--r--src/tac2tactics.ml3
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 =