1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i camlp4deps: "parsing/grammar.cma" i*)
11
(* $Id: g_congruence.ml4 10637 2008-03-07 23:52:56Z letouzey $ *)
17
(* Tactic registration *)
20
[ "congruence" ] -> [ congruence_tac 1000 [] ]
21
|[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
22
|[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
23
|[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
24
[ congruence_tac n l ]
28
[ "f_equal" ] -> [ f_equal ]