petits changements de syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 24 insertions, 16 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 276e033ac3..152b80e2a3 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -113,12 +113,18 @@ END
 (* AutoRewrite *)
 
 open Autorewrite
-TACTIC EXTEND Autorewrite
+TACTIC EXTEND AutorewriteV7
   [ "AutoRewrite" "[" ne_preident_list(l) "]" ] ->
     [ autorewrite Refiner.tclIDTAC l ]
 | [ "AutoRewrite" "[" ne_preident_list(l) "]" "using" tactic(t) ] ->
     [ autorewrite (snd t) l ]
 END
+TACTIC EXTEND AutorewriteV8
+  [ "AutoRewrite" "with" ne_preident_list(l) ] ->
+    [ autorewrite Refiner.tclIDTAC l ]
+| [ "AutoRewrite" "with" ne_preident_list(l) "using" tactic(t) ] ->
+    [ autorewrite (snd t) l ]
+END
 
 let add_rewrite_hint name ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
@@ -126,7 +132,7 @@ let add_rewrite_hint name ort t lcsr =
   add_rew_rules name (List.map f lcsr)
 
 (* V7 *)
-VERNAC COMMAND EXTEND HintRewrite_v7
+VERNAC COMMAND EXTEND HintRewriteV7
   [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) ] ->
   [ add_rewrite_hint b o Tacexpr.TacId l ]
 | [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b)
@@ -135,7 +141,7 @@ VERNAC COMMAND EXTEND HintRewrite_v7
 END
 
 (* V8 *)
-VERNAC COMMAND EXTEND HintRewrite
+VERNAC COMMAND EXTEND HintRewriteV8
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
   [ add_rewrite_hint b o Tacexpr.TacId l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0c0a0f592e..001e762d11 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -472,12 +472,8 @@ let apply_without_reduce c gl =
   let clause = mk_clenv_type_of wc c in 
   res_pf kONT clause gl
 
-(* Dead code
-let refinew_scheme kONT clause gl = res_pf kONT clause gl
-*)
-
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
-   |- B -> C and |- A (which is realized by Cut B;[Idtac|Apply c]
+   |- B -> C and |- A
 
    -------------------
    Gamma |- c : A -> B      Gamma |- ?2 : A
@@ -485,7 +481,13 @@ let refinew_scheme kONT clause gl = res_pf kONT clause gl
            Gamma |- B                        Gamma |- ?1 : B -> C
            -----------------------------------------------------
                              Gamma |- ? : C
- *)
+
+ Ltac lapply c :=
+  let ty := check c in
+  match eval hnf in ty with
+    ?A -> ?B => cut B; [ idtac | apply c ]
+  end.
+*)
 
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index c9a5c2cc01..4919dddac4 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -54,7 +54,7 @@ let is_disj ist =
 
 let not_dep_intros ist =
   <:tactic<
-  repeat match context with
+  repeat match goal with
   | |- (?X1 -> ?X2) => intro
   | |- (Coq.Init.Logic.iff _ _) => unfold Coq.Init.Logic.iff
   | |- (Coq.Init.Logic.not _)   => unfold Coq.Init.Logic.not
@@ -68,7 +68,7 @@ let axioms ist =
   let t_is_unit = tacticIn is_unit
   and t_is_empty = tacticIn is_empty in
     <:tactic<
-    match reverse context with
+    match reverse goal with
       | |- ?X1 => $t_is_unit; constructor 1
       | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
       | _:?X1 |- ?X1 => assumption
@@ -83,7 +83,7 @@ let simplif ist =
   <:tactic<
     $t_not_dep_intros;
     repeat
-       (match reverse context with
+       (match reverse goal with
         | id: (?X1 _ _) |- _ =>
             $t_is_conj; elim id; do 2 intro; clear id
         | id: (?X1 _ _) |- _ => $t_is_disj; elim id; intro; clear id
@@ -127,7 +127,7 @@ let rec tauto_intuit t_reduce solver ist =
   let t_solver = Tacexpr.TacArg (valueIn (VTactic (dummy_loc,solver))) in
   <:tactic<
    ($t_simplif;$t_axioms
-   || match reverse context with
+   || match reverse goal with
       | id:(?X1-> ?X2)-> ?X3|- _ =>
 	  cut X3;
 	    [ intro; clear id; $t_tauto_intuit 
@@ -140,7 +140,7 @@ let rec tauto_intuit t_reduce solver ist =
       end
     ||
     (* NB: [|- _ -> _] matches any product *)
-    match context with | |- _ -> _ => intro; $t_tauto_intuit
+    match goal with | |- _ -> _ => intro; $t_tauto_intuit
     |  |- _  => $t_reduce;$t_solver
     end
     ||
@@ -149,7 +149,7 @@ let rec tauto_intuit t_reduce solver ist =
     
 let reduction_not_iff=interp
  <:tactic<repeat 
-  match context with 
+  match goal with 
   | |- _     => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff 
   | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H
   end >>
@@ -173,7 +173,7 @@ let default_intuition_tac = interp <:tactic< auto with * >>
 
 let q_elim tac=
   <:tactic<
-  match context with 
+  match goal with 
     x : ?X1, H : ?X1 -> _ |- _ => generalize (H x); clear H; $tac
   end >>