Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg

2 files changed, 6 insertions, 4 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index 86251254..dc0dec0e 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
+(* $Id: cctac.ml 10121 2007-09-14 09:45:40Z corbinea $ *)
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
@@ -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 97fa4d77..ffc4b9c4 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cctac.mli 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: cctac.mli 10121 2007-09-14 09:45:40Z corbinea $ *)
 
 open Term 
 open Proof_type
 
+val proof_tac: Ccproof.proof -> Proof_type.tactic
+
 val cc_tactic : int -> constr list -> tactic
 
 val cc_fail : tactic