3 files changed, 23 insertions, 2 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index a9bd750c0..7a728f103 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -199,7 +199,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let ind=destInd h in 
   let types=Inductiveops.arities_of_constructors env ind in
   let lp=Array.length types in
-  let ci=(snd cstr)-1 in
+  let ci=pred (snd cstr) in
   let branch i=
     let ti=Term.prod_appvect types.(i) argv in
     let rc=fst (Sign.decompose_prod_assum ti) in
@@ -247,7 +247,7 @@ let rec proof_tac p gls =
 	and tx2=constr_of_term p2.p_rhs in
 	let typf = pf_type_of gls tf1 in
 	let typx = pf_type_of gls tx1 in
-	let typfx = prod_applist typf [tx1] in
+	let typfx = pf_type_of gls (mkApp (tf1,[|tx1|])) in
 	let id = pf_get_new_id (id_of_string "f") gls in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
index 58a0af41d..023525297 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -11,6 +11,8 @@
 open Term 
 open Proof_type
 
+val proof_tac: Ccproof.proof -> Proof_type.tactic
+
 val cc_tactic : int -> constr list -> tactic
 
 val cc_fail : tactic
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index 42df990fd..fecc89772 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -77,3 +77,22 @@ Theorem discr2 : Some true = Some false -> False.
 intros.
  congruence.
 Qed.
+
+Set Implicit Arguments.
+
+Parameter elt: Set.
+Parameter elt_eq: forall (x y: elt), {x = y} + {x <> y}.
+Definition t (A: Set) := elt -> A.
+Definition get (A: Set) (x: elt) (m: t A) := m x.
+Definition set (A: Set) (x: elt) (v: A) (m: t A) :=
+    fun (y: elt) => if elt_eq y x then v else m y.
+Lemma gsident:
+  forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
+Proof.
+  intros. unfold get, set. case (elt_eq j i); intro.
+  congruence.
+  auto.
+Qed.
+            
+            
+            
+\ No newline at end of file