Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 6 insertions, 97 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 66716acd..ee01f839 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extratactics.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: extratactics.ml4 11800 2009-01-18 18:34:15Z msozeau $ *)
 
 open Pp
 open Pcoq
@@ -18,6 +18,7 @@ open Mod_subst
 open Names
 open Tacexpr
 open Rawterm
+open Tactics
 
 (* Equality *)
 open Equality
@@ -133,10 +134,10 @@ let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings)
 
 TACTIC EXTEND conditional_rewrite
 | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
-    -> [ conditional_rewrite b (snd tac) c ]
+    -> [ conditional_rewrite b (snd tac) (inj_open (fst c), snd c) ]
 | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c)
     "in" hyp(h) ]
-    -> [ conditional_rewrite_in b h (snd tac) c ]
+    -> [ conditional_rewrite_in b h (snd tac) (inj_open (fst c), snd c) ]
 END
 
 TACTIC EXTEND dependent_rewrite
@@ -216,87 +217,6 @@ END
 
 let refine_tac = h_refine
 
-(* Setoid_replace *)
-
-open Setoid_replace
-
-(* TACTIC EXTEND setoid_replace *)
-(*    [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> *)
-(*      [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] *)
-(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> *)
-(*      [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] *)
-(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *)
-(*      [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] *)
-(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *)
-(*      [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] *)
-(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> *)
-(*      [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] *)
-(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> *)
-(*      [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] *)
-(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *)
-(*      [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] *)
-(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *)
-(*      [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] *)
-(* END *)
-
-(* TACTIC EXTEND setoid_rewrite *)
-(*    [ "setoid_rewrite" orient(b) constr(c) ] *)
-(*    -> [ general_s_rewrite b c ~new_goals:[] ] *)
-(*  | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ] *)
-(*    -> [ general_s_rewrite b c ~new_goals:l ] *)
-(*  | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] -> *)
-(*       [ general_s_rewrite_in h b c ~new_goals:[] ] *)
-(*  | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> *)
-(*       [ general_s_rewrite_in h b c ~new_goals:l ] *)
-(* END *)
-
-(* VERNAC COMMAND EXTEND AddSetoid1 *)
-(*   [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> *)
-(*    [ add_setoid n a aeq t ] *)
-(* | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> *)
-(*    [ new_named_morphism n m None ] *)
-(* | [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> *)
-(*    [ new_named_morphism n m (Some s)] *)
-(* END *)
-
-(* VERNAC COMMAND EXTEND AddRelation1 *)
-(*   [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *)
-(*    [ add_relation n a aeq (Some t) (Some t') None ] *)
-(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t)  "as" ident(n) ] -> *)
-(*    [ add_relation n a aeq (Some t) None None ] *)
-(* | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] -> *)
-(*    [ add_relation n a aeq None None None ] *)
-(* END *)
-
-(* VERNAC COMMAND EXTEND AddRelation2 *)
-(*   [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *)
-(*    [ add_relation n a aeq None (Some t') None ] *)
-(* | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'')  "as" ident(n) ] -> *)
-(*    [ add_relation n a aeq None (Some t') (Some t'') ] *)
-(* END *)
-
-(* VERNAC COMMAND EXTEND AddRelation3 *)
-(*   [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] -> *)
-(*    [ add_relation n a aeq (Some t) None (Some t') ] *)
-(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *)
-(*    [ add_relation n a aeq (Some t) (Some t') (Some t'') ] *)
-(* | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] -> *)
-(*    [ add_relation n a aeq None None (Some t) ] *)
-(* END *)
-
-(* TACTIC EXTEND setoid_symmetry *)
-(*    [ "setoid_symmetry" ] -> [ setoid_symmetry ] *)
-(*  | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] *)
-(* END *)
-
-(* TACTIC EXTEND setoid_reflexivity *)
-(*    [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] *)
-(* END *)
-
-(* TACTIC EXTEND setoid_transitivity *)
-(*    [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] *)
-(* END *)
-
 (* Inversion lemmas (Leminv) *)
 
 open Inv
@@ -485,17 +405,6 @@ END
 
 
 
-TACTIC EXTEND apply_in
-| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] -> 
-    [ apply_in false id cl ]
-END
-
-
-TACTIC EXTEND eapply_in
-| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] ->
-    [ apply_in true id cl ]
-END
-
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as 
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
@@ -505,8 +414,8 @@ TACTIC EXTEND generalize_eqs_vars
 | ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ]
 END
 
-TACTIC EXTEND conv
-| ["conv" constr(x) constr(y) ] -> [ conv x y ]
+TACTIC EXTEND dependent_pattern
+| ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ]
 END
 
 TACTIC EXTEND resolve_classes