From 9e87e9582ffe68ff549347d4fab37f7514992361 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 16 Dec 2016 18:38:20 +0100
Subject: 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'.
---
 ltac/g_auto.ml4 | 9 ---------
 1 file changed, 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)  ] -> [
-- 
cgit v1.2.3