diff options
author | 2006-11-21 21:38:49 +0000 | |
---|---|---|
committer | 2006-11-21 21:38:49 +0000 | |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /contrib/cc/g_congruence.ml4 | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'contrib/cc/g_congruence.ml4')
-rw-r--r-- | contrib/cc/g_congruence.ml4 | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4 index 0bdf7608..693aebb4 100644 --- a/contrib/cc/g_congruence.ml4 +++ b/contrib/cc/g_congruence.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: g_congruence.ml4 7734 2005-12-26 14:06:51Z herbelin $ *) +(* $Id: g_congruence.ml4 9151 2006-09-19 13:32:22Z corbinea $ *) open Cctac open Tactics @@ -17,13 +17,9 @@ open Tacticals (* Tactic registration *) TACTIC EXTEND cc - [ "congruence" ] -> [ tclORELSE - (tclTHEN (tclREPEAT introf) (cc_tactic [])) - cc_fail ] -END - -TACTIC EXTEND cc_with - [ "congruence" "with" ne_constr_list(l) ] -> [ tclORELSE - (tclTHEN (tclREPEAT introf) (cc_tactic l)) - cc_fail] + [ "congruence" ] -> [ congruence_tac 0 [] ] + |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] + |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 0 l ] + |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> + [ congruence_tac n l ] END |