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))