diff options
Diffstat (limited to 'tactics/coretactics.ml4')
| -rw-r--r-- | tactics/coretactics.ml4 | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 7da6df717..73b7bde9d 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 *) |