diff options
Diffstat (limited to 'plugins/ltac/tauto.ml')
| -rw-r--r-- | plugins/ltac/tauto.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4ec111e01..d8e21d81d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -220,9 +220,7 @@ let apply_nnpp _ ist = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> try - let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in - let nnpp = EConstr.of_constr nnpp in - apply nnpp + Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply with Not_found -> tclFAIL 0 (Pp.mt ()) end |