f_equal, revert, specialize in ML, contradict in better Ltac (+doc)

 * "f_equal" is now a tactic in ML (placed alongside congruence since
   it uses it). Normally, it should be completely compatible with the
   former Ltac version, except that it doesn't suffer anymore from the
   "up to 5 args" earlier limitation.

 * "revert" also becomes an ML tactic. This doesn't bring any real 
   improvement, just some more uniformity with clear and generalize.  

 * The experimental "narrow" tactic is removed from Tactics.v, and 
   replaced by an evolution of the old & undocumented "specialize" 
   ML tactic: 
   - when specialize is called on an hyp H, the specialization is 
     now done in place on H. For instance "specialize (H t u v)"
     removes the three leading forall of H and intantiates them by 
     t u and v.
   - otherwise specialize still works as before (i.e. as a kind of 
     generalize).
   See the RefMan and test-suite/accept/specialize.v for more infos. 
   Btw, specialize can still accept an optional number for specifying 
   how many premises to instantiate. This number should normally 
   be useless now (some autodetection mecanism added). Hence this 
   feature is left undocumented. For the happy few still using 
   specialize in the old manner, beware of the slight incompatibities...

 * finally, "contradict" is left as Ltac in Tactics.v, but it has 
   now a better shape (accepts unfolded nots and/or things in Type), 
   and also some documentation in the RefMan



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

1 files changed, 48 insertions, 0 deletions

diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
new file mode 100644
index 000000000..4929ae4c0
--- /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