diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 27 | ||||
| -rw-r--r-- | tactics/extratactics.mli | 13 |
2 files changed, 26 insertions, 14 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 521bf5409..41b79fefb 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -50,10 +50,15 @@ let pr_by_arg_tac _prc _prlc prtac opt_c = n'ai pas reussi *) +let pr_in_hyp = function + | None -> mt () + | Some id -> spc () ++ hov 2 (str "in" ++ spc () ++ Nameops.pr_id id) + let pr_in_arg_hyp _prc _prlc _prtac opt_c = - match opt_c with - | None -> mt () - | Some id -> spc () ++ hov 2 (str "by" ++ spc () ++ Nameops.pr_id id) + pr_in_hyp (Util.option_map snd opt_c) + +let pr_in_arg_hyp_typed _prc _prlc _prtac = + pr_in_hyp ARGUMENT EXTEND by_arg_tac TYPED AS tactic_opt @@ -63,9 +68,13 @@ ARGUMENT EXTEND by_arg_tac END ARGUMENT EXTEND in_arg_hyp - TYPED AS ident_opt - PRINTED BY pr_in_arg_hyp -| [ "in" ident(c) ] -> [ Some (c) ] + TYPED AS var_opt + PRINTED BY pr_in_arg_hyp_typed + RAW_TYPED AS var_opt + RAW_PRINTED BY pr_in_arg_hyp + GLOB_TYPED AS var_opt + GLOB_PRINTED BY pr_in_arg_hyp +| [ "in" hyp(c) ] -> [ Some (c) ] | [ ] -> [ None ] END @@ -183,9 +192,9 @@ TACTIC EXTEND autorewrite [ autorewrite Refiner.tclIDTAC l ] | [ "autorewrite" "with" ne_preident_list(l) "using" tactic(t) ] -> [ autorewrite (snd t) l ] -| [ "autorewrite" "with" ne_preident_list(l) "in" ident(id) ] -> +| [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) ] -> [ autorewrite_in id Refiner.tclIDTAC l ] -| [ "autorewrite" "with" ne_preident_list(l) "in" ident(id) "using" tactic(t) ] -> +| [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) "using" tactic(t) ] -> [ autorewrite_in id (snd t) l ] END @@ -283,7 +292,7 @@ END TACTIC EXTEND setoid_symmetry [ "setoid_symmetry" ] -> [ setoid_symmetry ] - | [ "setoid_symmetry" "in" ident(n) ] -> [ setoid_symmetry_in n ] + | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] END TACTIC EXTEND setoid_reflexivity diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index c9252d4e3..ce9bff52c 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -8,10 +8,14 @@ (*i $Id$ i*) +open Util open Names open Term open Proof_type open Rawterm +open Tacexpr +open Topconstr +open Genarg val h_discrHyp : quantified_hypothesis -> tactic val h_injHyp : quantified_hypothesis -> tactic @@ -26,14 +30,13 @@ val refine_tac : Genarg.open_constr -> tactic *) -val rawwit_in_arg_hyp: identifier option Tacexpr.raw_abstract_argument_type -val in_arg_hyp: identifier option Pcoq.Gram.Entry.e +val rawwit_in_arg_hyp: identifier located option raw_abstract_argument_type + +val in_arg_hyp: identifier located option Pcoq.Gram.Entry.e val rawwit_by_arg_tac : - (Tacexpr.raw_tactic_expr option, Topconstr.constr_expr, - Tacexpr.raw_tactic_expr) - Genarg.abstract_argument_type + (raw_tactic_expr option, constr_expr, raw_tactic_expr) abstract_argument_type val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e |