diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 5 | ||||
| -rw-r--r-- | ltac/extraargs.ml4 | 14 | ||||
| -rw-r--r-- | ltac/extraargs.mli | 5 |
3 files changed, 23 insertions, 1 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index de4d589ee..618666758 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -151,7 +151,10 @@ END TACTIC EXTEND symmetry [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] -| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ] +END + +TACTIC EXTEND symmetry_in +| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ] END (** Split *) diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index c6d72e03e..0db1cd7ba 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -260,6 +260,20 @@ END let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c +let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl +let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl +let in_clause' = Pcoq.Tactic.in_clause + +ARGUMENT EXTEND in_clause + TYPED AS clause_dft_concl + PRINTED BY pr_in_top_clause + RAW_TYPED AS clause_dft_concl + RAW_PRINTED BY pr_in_clause + GLOB_TYPED AS clause_dft_concl + GLOB_PRINTED BY pr_in_clause +| [ in_clause'(cl) ] -> [ cl ] +END + (* spiwack: the print functions are incomplete, but I don't know what they are used for *) let pr_r_nat_field natf = diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 0cf77935c..b12187e18 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -71,3 +71,8 @@ val pr_by_arg_tac : val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type + +val wit_in_clause : + (Id.t Loc.located Locus.clause_expr, + Id.t Loc.located Locus.clause_expr, + Id.t Locus.clause_expr) Genarg.genarg_type |