diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/dependentind.v | 6 | ||||
| -rw-r--r-- | test-suite/success/specialize.v | 48 |
2 files changed, 51 insertions, 3 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index f45b592af8..77bc295fd8 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -67,7 +67,7 @@ Proof with simpl in * ; auto ; simpl_depind. apply ax. destruct D... - narrow IHterm with G empty... + specialize (IHterm G empty)... apply weak... apply weak... @@ -76,7 +76,7 @@ Proof with simpl in * ; auto ; simpl_depind. apply weak ; apply abs ; apply H. apply abs... - narrow IHterm with G0 (D, t, tau)... + specialize (IHterm G0 (D, t, tau))... apply app with tau... Qed. @@ -97,7 +97,7 @@ Proof with simpl in * ; simpl_depind ; auto. apply weak... apply abs... - narrow IHterm with G0 (D, tau)... + specialize (IHterm G0 (D, tau))... eapply app with tau... Save. diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v new file mode 100644 index 0000000000..4929ae4c0c --- /dev/null +++ b/test-suite/success/specialize.v @@ -0,0 +1,48 @@ + +Goal forall a b c : nat, a = b -> b = c -> forall d, a+d=c+d. +intros. + +(* "compatibility" mode: specializing a global name + means a kind of generalize *) + +specialize trans_equal. intros _. +specialize trans_equal with (1:=H)(2:=H0). intros _. +specialize trans_equal with (x:=a)(y:=b)(z:=c). intros _. +specialize trans_equal with (1:=H)(z:=c). intros _. +specialize trans_equal with nat a b c. intros _. +specialize (@trans_equal nat). intros _. +specialize (@trans_equal _ a b c). intros _. +specialize (trans_equal (x:=a)). intros _. +specialize (trans_equal (x:=a)(y:=b)). intros _. +specialize (trans_equal H H0). intros _. +specialize (trans_equal H0 (z:=b)). intros _. + +(* local "in place" specialization *) +assert (Eq:=trans_equal). + +specialize Eq. +specialize Eq with (1:=H)(2:=H0). Undo. +specialize Eq with (x:=a)(y:=b)(z:=c). Undo. +specialize Eq with (1:=H)(z:=c). Undo. +specialize Eq with nat a b c. Undo. +specialize (Eq nat). Undo. +specialize (Eq _ a b c). Undo. +(* no implicit argument for Eq, hence no (Eq (x:=a)) *) +specialize (Eq _ _ _ _ H H0). Undo. +specialize (Eq _ _ _ b H0). Undo. + +(* +(** strange behavior to inspect more precisely *) + +(* 1) proof aspect : let H:= ... in (fun H => ..) H + presque ok... *) + +(* 2) echoue moins lorsque zero premise de mangé *) +specialize trans_equal with (1:=Eq). (* mal typé !! *) + +(* 3) *) +specialize trans_equal with _ a b c. intros _. +(* Anomaly: Evar ?88 was not declared. Please report. *) +*) + +Abort.
\ No newline at end of file |