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

5 files changed, 36 insertions, 1 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index e90e7afaa2..8eda68e106 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -430,3 +430,29 @@ let congruence_tac depth l =
   tclORELSE 
     (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) 
     cc_fail
+
+(* The [f_equal] tactic.
+
+   It mimics the use of lemmas [f_equal], [f_equal2], etc.
+   This isn't particularly related with congruence, apart from
+   the fact that congruence is called internally. 
+*)
+
+let f_equal gl = 
+  let cut_eq c1 c2 = 
+    tclTHENTRY
+      (Tactics.cut (mkApp (Lazy.force _eq, [| pf_type_of gl c1; c1; c2|])))
+      reflexivity
+  in 
+  try match kind_of_term (pf_concl gl) with 
+    | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> 
+	begin match kind_of_term t, kind_of_term t' with 
+	  | App (f,v), App (f',v') when Array.length v = Array.length v' ->
+	      let rec cuts i = 
+		if i < 0 then tclTRY (congruence_tac 1000 []) 
+		else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+	      in cuts (Array.length v - 1) gl
+	  | _ -> tclIDTAC gl
+	end
+    | _ -> tclIDTAC gl
+  with Type_errors.TypeError _ -> tclIDTAC gl
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
index 0235252975..7cdd46ab4a 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -18,3 +18,5 @@ val cc_tactic : int -> constr list -> tactic
 val cc_fail : tactic
 
 val congruence_tac : int -> constr list -> tactic
+
+val f_equal : tactic
diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4
index 5b2cff9c27..f23ed49b6e 100644
--- a/contrib/cc/g_congruence.ml4
+++ b/contrib/cc/g_congruence.ml4
@@ -23,3 +23,7 @@ TACTIC EXTEND cc
  |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> 
    [ congruence_tac n l ]
 END
+
+TACTIC EXTEND f_equal
+ [ "f_equal" ] -> [ f_equal ]
+END
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index a0cbe22b36..16357fc472 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -340,7 +340,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacClear     _
     | TacClearBody _
     | TacMove      _
-    | TacRename    _ -> acc
+    | TacRename    _ 
+    | TacRevert    _ -> acc
 
     (* Constructors *)
     | TacLeft        cb
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c5a8c756a8..2219e327ca 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1187,6 +1187,7 @@ and xlate_tac =
        let idl' = List.map xlate_hyp idl in
        CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
     | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
+    | TacRevert _ -> xlate_error "TODO: revert"
     | (*For translating tactics/Inv.v *)
       TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
 	CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
@@ -1248,6 +1249,7 @@ and xlate_tac =
 	  (CT_formula_list
 	     (List.map xlate_formula
 		(out_gen (wit_list0 rawwit_constr) args)))
+    | TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal"
     | TacExtend (_,id, l) ->
 	print_endline ("Extratactics : "^ id);
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))