diff options
| author | Théo Zimmermann | 2016-12-16 18:38:20 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-02-07 17:38:00 +0100 |
| commit | 9e87e9582ffe68ff549347d4fab37f7514992361 (patch) | |
| tree | 8c0d636d83a30301045894c2c500f2e29407e0f4 | |
| parent | 5e909ab948ea3db4b5d734ec1c68198874c9724c (diff) | |
Remove hackish autounfoldify now that hintdb can be bound to Ltac variables.
It will be possible to replace any call to 'autounfoldify x' with 'autounfold with x'.
| -rw-r--r-- | ltac/g_auto.ml4 | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index a37cf306e1..4ec42c676f 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -149,15 +149,6 @@ TACTIC EXTEND autounfold_one [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ] END -TACTIC EXTEND autounfoldify -| [ "autounfoldify" constr(x) ] -> [ - let db = match Term.kind_of_term x with - | Term.Const (c,_) -> Names.Label.to_string (Names.con_label c) - | _ -> assert false - in Eauto.autounfold ["core";db] Locusops.onConcl - ] -END - TACTIC EXTEND unify | ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] | ["unify" constr(x) constr(y) "with" preident(base) ] -> [ |