summaryrefslogtreecommitdiff
path: root/tactics/extratactics.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /tactics/extratactics.ml4
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'tactics/extratactics.ml4')
-rw-r--r--tactics/extratactics.ml439
1 files changed, 15 insertions, 24 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a9ee65d7..48bd87ee 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: extratactics.ml4 8651 2006-03-21 21:54:43Z jforest $ *)
+(* $Id: extratactics.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
open Pp
open Pcoq
@@ -20,6 +20,9 @@ open Names
(* Equality *)
open Equality
+(* Pierre L: for an easy implementation of "rewrite ... in <clause>", rewrite
+ has moved to g_tactics.ml4
+
TACTIC EXTEND rewrite
| [ "rewrite" orient(b) constr_with_bindings(c) ] ->
[general_rewrite_bindings b c]
@@ -30,57 +33,45 @@ TACTIC EXTEND rewrite_in
[general_rewrite_bindings_in b h c]
END
-let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
+let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
+*)
(* Julien: Mise en commun des differentes version de replace with in by
- TODO: améliorer l'affichage et deplacer dans extraargs
+ TODO: deplacer dans extraargs
*)
-
-let pr_by_arg_tac prc _ _ opt_c =
+let pr_by_arg_tac _prc _prlc prtac opt_c =
match opt_c with
| None -> mt ()
- | Some c -> spc () ++ hov 2 (str "by" ++ spc () )
+ | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
(* Julien Forest: on voudrait pouvoir passer la loc mais je
n'ai pas reussi
*)
-let pr_in_arg_hyp =
-fun prc _ _ opt_c->
+let pr_in_arg_hyp _prc _prlc _prtac opt_c =
match opt_c with
| None -> mt ()
- | Some c ->
- spc () ++ hov 2 (str "by" ++ spc () ++
- Pptactic.pr_or_var (fun _ -> mt ())
- (ArgVar(Util.dummy_loc,c))
- )
-
-
-
+ | Some id -> spc () ++ hov 2 (str "by" ++ spc () ++ Nameops.pr_id id)
ARGUMENT EXTEND by_arg_tac
TYPED AS tactic_opt
PRINTED BY pr_by_arg_tac
-| [ "by" tactic(c) ] -> [ Some c ]
+| [ "by" tactic3(c) ] -> [ Some c ]
| [ ] -> [ None ]
END
ARGUMENT EXTEND in_arg_hyp
TYPED AS ident_opt
PRINTED BY pr_in_arg_hyp
-| [ "in" int_or_var(c) ] ->
- [ match c with
- | ArgVar(_,c) -> Some (c)
- | _ -> Util.error "in must be used with an identifier"
- ]
+| [ "in" ident(c) ] -> [ Some (c) ]
| [ ] -> [ None ]
END
TACTIC EXTEND replace
-| ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] ->
- [ new_replace c1 c2 in_hyp (Util.option_app Tacinterp.eval_tactic tac) ]
+ ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
+-> [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac) ]
END
(* Julien: