diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-30 09:47:54 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-30 09:47:54 +0000 |
| commit | 534cbe4f02392c45567ea30d02b53751482ed767 (patch) | |
| tree | 551492b23a09f05a41e65fe60040cdfd40e761a3 /tactics/auto.mli | |
| parent | a99754e41a7b80d2e2a464e6614ccf3026ef4df0 (diff) | |
Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl
No grammar entries for these tactics since coq 8.0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15102 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index bd425c1de..95de089e0 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -103,8 +103,6 @@ type hints_entry = | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsExternEntry of int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr - | HintsDestructEntry of identifier * int * (bool,unit) Tacexpr.location * - (patvar list * constr_pattern) * Tacexpr.glob_tactic_expr val searchtable_map : hint_db_name -> hint_db @@ -255,7 +253,7 @@ val h_trivial : open_constr list -> hint_db_name list option -> tactic val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds -(** {6 The following is not yet up to date -- Papageno. } *) +(** Destructing Auto *) (** DAuto *) val dauto : int option * int option -> open_constr list -> tactic @@ -264,16 +262,6 @@ val default_dauto : tactic val h_dauto : int option * int option -> open_constr list -> tactic -(** SuperAuto *) - -type autoArguments = - | UsingTDB - | Destructing - -(* -val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic -*) - -val h_superauto : int option -> reference list -> bool -> bool -> tactic +(** Hook for changing the initialization of auto *) val add_auto_init : (unit -> unit) -> unit |