aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/nsatz')
-rw-r--r--plugins/nsatz/g_nsatz.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 0da630530..5f906a8da 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -13,5 +13,5 @@ DECLARE PLUGIN "nsatz_plugin"
DECLARE PLUGIN "nsatz_plugin"
TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute" constr(lt) ] -> [ Proofview.V82.tactic (Nsatz.nsatz_compute lt) ]
+| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute lt ]
END