(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* [ congruence_tac 1000 [] ] |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> [ congruence_tac n l ] END TACTIC EXTEND f_equal [ "f_equal" ] -> [ f_equal ] END