diff options
author | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
commit | e4282ea99c664d8d58067bee199cbbcf881b60d5 (patch) | |
tree | d4c4a873eb055c728666f367469fa26c3417793a /tactics/hiddentac.ml | |
parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) |
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'tactics/hiddentac.ml')
-rw-r--r-- | tactics/hiddentac.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index b270ba2d..8e517453 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hiddentac.ml 11671 2008-12-12 12:43:03Z herbelin $ *) +(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *) open Term open Proof_type @@ -75,10 +75,6 @@ let h_generalize_dep c = let h_let_tac b na c cl = let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl) -let h_instantiate n c ido = -(Evar_tactics.instantiate n c ido) - (* abstract_tactic (TacInstantiate (n,c,cls)) - (Evar_refiner.instantiate n c (simple_clause_of cls)) *) (* Derived basic tactics *) let h_simple_induction_destruct isrec h = |