summaryrefslogtreecommitdiff
path: root/contrib/cc/cctac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/cc/cctac.ml')
-rw-r--r--contrib/cc/cctac.ml6
1 files changed, 3 insertions, 3 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 =