aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/g_congruence.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc/g_congruence.ml4')
-rw-r--r--plugins/cc/g_congruence.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index b787e824f..6f6811334 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -18,9 +18,9 @@ DECLARE PLUGIN "cc_plugin"
TACTIC EXTEND cc
[ "congruence" ] -> [ congruence_tac 1000 [] ]
|[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 (List.map EConstr.of_constr l) ]
+ |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
|[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
- [ congruence_tac n (List.map EConstr.of_constr l) ]
+ [ congruence_tac n l ]
END
TACTIC EXTEND f_equal