diff options
Diffstat (limited to 'tactics/coretactics.ml4')
| -rw-r--r-- | tactics/coretactics.ml4 | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 7da6df717e..6c02a7202f 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -13,6 +13,12 @@ open Names open Locus open Misctypes open Genredexpr +open Stdarg +open Constrarg +open Extraargs +open Pcoq.Constr +open Pcoq.Prim +open Pcoq.Tactic open Proofview.Notations open Sigma.Notations @@ -143,7 +149,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 *) |