diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 7 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 4 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 1 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 7 | ||||
| -rw-r--r-- | tactics/g_auto.ml4 | 7 | ||||
| -rw-r--r-- | tactics/g_class.ml4 | 5 | ||||
| -rw-r--r-- | tactics/g_rewrite.ml4 | 5 |
7 files changed, 33 insertions, 3 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 7da6df717e..73b7bde9d7 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -13,6 +13,11 @@ open Names open Locus open Misctypes open Genredexpr +open Stdarg +open Constrarg +open Pcoq.Constr +open Pcoq.Prim +open Pcoq.Tactic open Proofview.Notations open Sigma.Notations @@ -143,7 +148,7 @@ END TACTIC EXTEND symmetry [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] -| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ] +| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ] END (** Split *) diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 98868e8f91..8215e785ab 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -10,6 +10,10 @@ open Pp open Genarg +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr open Names open Tacexpr open Taccoerce diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 7df845e4bd..f7b379e69e 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -53,7 +53,6 @@ val pr_by_arg_tac : (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> raw_tactic_expr option -> Pp.std_ppcmds - (** Spiwack: Primitive for retroknowledge registration *) val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index ae8b83b95e..52419497d1 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -10,7 +10,12 @@ open Pp open Genarg +open Stdarg +open Constrarg open Extraargs +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic open Mod_subst open Names open Tacexpr @@ -49,6 +54,8 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac = let replace_term ist dir_opt c cl = with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) +let clause = Pcoq.Tactic.clause_dft_concl + TACTIC EXTEND replace ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ] diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4 index f4fae763fd..788443944f 100644 --- a/tactics/g_auto.ml4 +++ b/tactics/g_auto.ml4 @@ -10,6 +10,11 @@ open Pp open Genarg +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic open Tacexpr DECLARE PLUGIN "g_auto" @@ -128,7 +133,7 @@ TACTIC EXTEND dfs_eauto END TACTIC EXTEND autounfold -| [ "autounfold" hintbases(db) clause(cl) ] -> [ Eauto.autounfold_tac db cl ] +| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ] END TACTIC EXTEND autounfold_one diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index 766593543c..9ef1545416 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -10,6 +10,11 @@ open Misctypes open Class_tactics +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic +open Stdarg +open Constrarg DECLARE PLUGIN "g_class" diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 0ce886373f..c4ef1f297e 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -20,6 +20,11 @@ open Extraargs open Tacmach open Tacticals open Rewrite +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "g_rewrite" |