aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/g_omega.mlg2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg
index c3d063cff8..85081b24a3 100644
--- a/plugins/omega/g_omega.mlg
+++ b/plugins/omega/g_omega.mlg
@@ -27,7 +27,7 @@ open Stdarg
let eval_tactic name =
let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
- let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
+ let kn = KerName.make (ModPath.MPfile dp) (Label.make name) in
let tac = Tacenv.interp_ltac kn in
Tacinterp.eval_tactic tac