diff options
Diffstat (limited to 'plugins/ltac/extratactics.mlg')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4f20e5a800..a2a47c0bf4 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -33,8 +33,6 @@ open Proofview.Notations open Attributes open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" @@ -450,7 +448,7 @@ END (* Subst *) TACTIC EXTEND subst -| [ "subst" ne_var_list(l) ] -> { subst l } +| [ "subst" ne_hyp_list(l) ] -> { subst l } | [ "subst" ] -> { subst_all () } END |