diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/dune | 1 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 3 |
2 files changed, 3 insertions, 1 deletions
@@ -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 = |