3 files changed, 12 insertions, 8 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 4a691e442c..ce620d5312 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -460,7 +460,7 @@ let rec canonize_name sigma c =
           mkApp (func ct,Array.Smart.map func l)
       | Proj(p,c) ->
 	let p' = Projection.map (fun kn ->
-          Constant.make1 (Constant.canonical kn)) p in 
+          MutInd.make1 (MutInd.canonical kn)) p in
 	  (mkProj (p', func c))
       | _ -> c
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 04ff11fc49..2eaa6146e1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -84,8 +84,8 @@ let rec decompose_term env sigma t=
 	let canon_const = Constant.make1 (Constant.canonical c) in 
 	  (Symb (Constr.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
-	let canon_const kn = Constant.make1 (Constant.canonical kn) in 
-	let p' = Projection.map canon_const p in
+        let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in
+        let p' = Projection.map canon_mind p in
 	let c = Retyping.expand_projection env sigma p' c [] in
 	decompose_term env sigma c
     | _ ->
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