diff options
| -rw-r--r-- | plugins/interface/xlate.ml | 15 | ||||
| -rw-r--r-- | tactics/equality.ml | 13 | ||||
| -rw-r--r-- | tactics/equality.mli | 4 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | test-suite/parser/obj_magic.out | 120 | ||||
| -rw-r--r-- | test-suite/parser/obj_magic.v | 4 | ||||
| -rw-r--r-- | theories/ZArith/Zlogarithm.v | 15 |
7 files changed, 99 insertions, 80 deletions
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 1f4038cbb..6f9e673a9 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -1039,21 +1039,6 @@ and xlate_tac = | TacRewrite(_,_,_,Some _) -> xlate_error "TODO: rewrite by" | TacRewrite(false,_,cl,_) -> xlate_error "TODO: rewrite of several hyps at once" | TacRewrite(true,_,cl,_) -> xlate_error "TODO: erewrite" - | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) -> - let t = out_gen rawwit_main_tactic t in - let b = out_gen Extraargs.rawwit_orient b in - let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in - let c = xlate_formula c and bindl = xlate_bindings bindl in - if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE) - else CT_condrewrite_rl (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE) - | TacExtend (_,"conditional_rewrite", [t; b; cbindl; id]) -> - let t = out_gen rawwit_main_tactic t in - let b = out_gen Extraargs.rawwit_orient b in - let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in - let c = xlate_formula c and bindl = xlate_bindings bindl in - let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in - if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, id) - else CT_condrewrite_rl (xlate_tactic t, c, bindl, id) | TacExtend (_,"dependent_rewrite", [b; c]) -> let b = out_gen Extraargs.rawwit_orient b in let c = xlate_formula (out_gen rawwit_constr c) in diff --git a/tactics/equality.ml b/tactics/equality.ml index 89a3704ee..3cf5cfd73 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -290,22 +290,9 @@ let general_multi_multi_rewrite with_evars l cl tac = | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l) in loop l -(* Conditional rewriting, the success of a rewriting is related - to the resolution of the conditions by a given tactic *) - -let conditional_rewrite lft2rgt tac (c,bl) = - tclTHENSFIRSTn - (general_rewrite_ebindings lft2rgt all_occurrences (c,bl) false) - [|tclIDTAC|] (tclCOMPLETE tac) - let rewriteLR = general_rewrite true all_occurrences let rewriteRL = general_rewrite false all_occurrences -let conditional_rewrite_in lft2rgt id tac (c,bl) = - tclTHENSFIRSTn - (general_rewrite_ebindings_in lft2rgt all_occurrences id (c,bl) false) - [|tclIDTAC|] (tclCOMPLETE tac) - (* Replacing tactics *) (* eq,sym_eq : equality on Type and its symmetry theorem diff --git a/tactics/equality.mli b/tactics/equality.mli index deb68aac8..a52d06499 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -64,10 +64,6 @@ val general_multi_multi_rewrite : evars_flag -> (bool * multi * open_constr with_bindings) list -> clause -> (tactic * conditions) option -> tactic -val conditional_rewrite : orientation -> tactic -> open_constr with_bindings -> tactic -val conditional_rewrite_in : - orientation -> identifier -> tactic -> open_constr with_bindings -> tactic - val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic val replace : constr -> constr -> tactic val replace_in : identifier -> constr -> constr -> tactic diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6676b90ac..2b4b9cffe 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -134,14 +134,6 @@ END 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) (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) (inj_open (fst c), snd c) ] -END - TACTIC EXTEND dependent_rewrite | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] | [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ] diff --git a/test-suite/parser/obj_magic.out b/test-suite/parser/obj_magic.out index edd1e751b..302fd6bb5 100644 --- a/test-suite/parser/obj_magic.out +++ b/test-suite/parser/obj_magic.out @@ -51,6 +51,9 @@ n vernac$absurd 1 n +vernac$try +1 +n vernac$none 0 n @@ -76,17 +79,11 @@ vernac$int 1 a vernac$ident -deq -a -vernac$ident H n -vernac$tactic_arg_list +vernac$simplify_eq 1 n -vernac$simple_user_tac -2 -n vernac$none 0 n @@ -117,12 +114,24 @@ a vernac$ident b n -vernac$replace_with +vernac$hyp_location_list +0 +n +vernac$star +0 +n +vernac$clause 2 n vernac$none 0 n +vernac$replace_with +4 +n +vernac$none +0 +n vernac$solve 3 a @@ -144,9 +153,15 @@ n vernac$binding_list 1 n -vernac$none +vernac$hyp_location_list +0 +n +vernac$star 0 n +vernac$clause +2 +n vernac$rewrite_rl 3 n @@ -177,6 +192,15 @@ a vernac$ident H1 n +vernac$hyp_location_list +1 +n +vernac$none +0 +n +vernac$clause +2 +n vernac$rewrite_rl 3 n @@ -188,12 +212,6 @@ vernac$solve a vernac$int 1 -n -vernac$none -0 -n -vernac$auto -1 a vernac$ident H @@ -210,11 +228,17 @@ n vernac$binding_list 1 n -vernac$none +vernac$hyp_location_list 0 n -vernac$condrewrite_lr -4 +vernac$star +0 +n +vernac$clause +2 +n +vernac$rewrite_lr +3 n vernac$none 0 @@ -224,12 +248,6 @@ vernac$solve a vernac$int 1 -n -vernac$none -0 -n -vernac$auto -1 a vernac$ident H @@ -249,8 +267,17 @@ a vernac$ident H2 n -vernac$condrewrite_lr -4 +vernac$hyp_location_list +1 +n +vernac$none +0 +n +vernac$clause +2 +n +vernac$rewrite_lr +3 n vernac$none 0 @@ -306,6 +333,36 @@ a vernac$int 1 a +vernac$string +_ = _ +a +vernac$ident +a +a +vernac$ident +b +n +vernac$formula_list +2 +n +vernac$notation +2 +a +vernac$ident +H +n +vernac$cutrewrite_lr +2 +n +vernac$none +0 +n +vernac$solve +3 +a +vernac$int +1 +a vernac$int 3 a @@ -466,16 +523,19 @@ vernac$int 1 a vernac$ident +ring +a +vernac$ident a a vernac$ident b n -vernac$formula_list +vernac$tactic_arg_list 2 n -vernac$ring -1 +vernac$simple_user_tac +2 n vernac$none 0 @@ -544,6 +604,6 @@ vernac$hintrewrite 4 n vernac$command_list -20 +21 e blabla diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v index 7d60bbd97..7f0c23af6 100644 --- a/test-suite/parser/obj_magic.v +++ b/test-suite/parser/obj_magic.v @@ -6,8 +6,8 @@ injection H. replace a with b. rewrite <- H with (a := b). rewrite <- H with (a := b) in H1. -conditional (auto) rewrite H with (1 := b). -conditional (auto) rewrite H with (1 := b) in H2. +rewrite H with (1 := b). +rewrite H with (1 := b) in H2. dependent rewrite H. cutrewrite (a = b). cutrewrite (a = b) in H. diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 18d1bba97..68e9c7733 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -54,20 +54,19 @@ Section Log_pos. (* Log of positive integers *) Theorem log_inf_correct : forall x:positive, 0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Zsucc (log_inf x)). + Proof. simple induction x; intros; simpl in |- *; [ elim H; intros Hp HR; clear H; split; [ auto with zarith - | conditional apply Zle_le_succ; trivial rewrite - two_p_S with (x := Zsucc (log_inf p)); - conditional trivial rewrite two_p_S; - conditional trivial rewrite two_p_S in HR; rewrite (BinInt.Zpos_xI p); + | rewrite two_p_S with (x := Zsucc (log_inf p)) by (apply Zle_le_succ; trivial); + rewrite two_p_S by trivial; + rewrite two_p_S in HR by trivial; rewrite (BinInt.Zpos_xI p); omega ] | elim H; intros Hp HR; clear H; split; [ auto with zarith - | conditional apply Zle_le_succ; trivial rewrite - two_p_S with (x := Zsucc (log_inf p)); - conditional trivial rewrite two_p_S; - conditional trivial rewrite two_p_S in HR; rewrite (BinInt.Zpos_xO p); + | rewrite two_p_S with (x := Zsucc (log_inf p)) by (apply Zle_le_succ; trivial); + rewrite two_p_S by trivial; + rewrite two_p_S in HR by trivial; rewrite (BinInt.Zpos_xO p); omega ] | unfold two_power_pos in |- *; unfold shift_pos in |- *; simpl in |- *; omega ]. |