Merge PR #7979: TACTIC EXTEND in coqpp

1 files changed, 9 insertions, 5 deletions

diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.mlg
index fb013ac131..685059294f 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.mlg
@@ -8,22 +8,26 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open Cctac
 open Stdarg
 
+}
+
 DECLARE PLUGIN "cc_plugin"
 
 (* Tactic registration *)
 
 TACTIC EXTEND cc
- [ "congruence" ] -> [ congruence_tac 1000 [] ]
- |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
+| [ "congruence" ] -> { 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 ]
+   { congruence_tac n l }
 END
 
 TACTIC EXTEND f_equal
- [ "f_equal" ] -> [ f_equal ]
+| [ "f_equal" ] -> { f_equal }
 END