diff options
| author | Pierre-Marie Pédrot | 2016-06-03 17:10:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-03 17:11:07 +0200 |
| commit | 89a1ea67a72500eeae1d003dd346f01ded514f7b (patch) | |
| tree | 8134c12bef64decc00490519f2f04e06932355e0 /theories | |
| parent | 9d60ddc84e95a030913fc4b3db705f3ec894fdb2 (diff) | |
| parent | 3206bf597d63066d9d9f8adfd0fe76e3c1c97e4d (diff) | |
Remove a few tactics from the Tacexpr AST.
Note that this breaks a few badly written scripts using intro in strict
mode without providing an existing identifier.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 1 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis_reg.v | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index cc023cc3f8..a3c265a21f 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -417,6 +417,7 @@ Local Open Scope Int_scope. Let's do its job by hand: *) Ltac join_tac := + let l := fresh "l" in intro l; induction l as [| lh ll _ lx lr Hlr]; [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join; [ | destruct ((rh+2) <? lh) eqn:LT; diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index e57af7311f..0c27d407c3 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -109,6 +109,7 @@ Ltac intro_hyp_glob trm := | Rabs => idtac | ?X1 => let p := constr:(X1) in + let HYPPD := fresh "HYPPD" in match goal with | _:(derivable p) |- _ => idtac | |- (derivable p) => idtac @@ -250,6 +251,7 @@ Ltac intro_hyp_pt trm pt := end | ?X1 => let p := constr:(X1) in + let HYPPD := fresh "HYPPD" in match goal with | _:(derivable_pt p pt) |- _ => idtac | |- (derivable_pt p pt) => idtac @@ -341,8 +343,10 @@ Ltac is_diff_pt := | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) => assumption | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) => + let HypDDPT := fresh "HypDDPT" in cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ] | |- (True -> derivable_pt _ _) => + let HypTruE := fresh "HypTruE" in intro HypTruE; clear HypTruE; is_diff_pt | _ => try @@ -411,6 +415,7 @@ Ltac is_diff_glob := apply (derivable_comp X2 X1); is_diff_glob | _:(derivable ?X1) |- (derivable ?X1) => assumption | |- (True -> derivable _) => + let HypTruE := fresh "HypTruE" in intro HypTruE; clear HypTruE; is_diff_glob | _ => try @@ -490,14 +495,17 @@ Ltac is_cont_pt := | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) => assumption | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) => + let HypDDPT := fresh "HypDDPT" in cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ] | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) => apply derivable_continuous_pt; assumption | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) => + let HypDDPT := fresh "HypDDPT" in cut (continuity X1); [ intro HypDDPT; apply HypDDPT | apply derivable_continuous; assumption ] | |- (True -> continuity_pt _ _) => + let HypTruE := fresh "HypTruE" in intro HypTruE; clear HypTruE; is_cont_pt | _ => try @@ -567,6 +575,7 @@ Ltac is_cont_glob := apply (continuity_comp X2 X1); try is_cont_glob || assumption | _:(continuity ?X1) |- (continuity ?X1) => assumption | |- (True -> continuity _) => + let HypTruE := fresh "HypTruE" in intro HypTruE; clear HypTruE; is_cont_glob | _:(derivable ?X1) |- (continuity ?X1) => apply derivable_continuous; assumption |