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

3 files changed, 34 insertions, 25 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 58dda021..1f7bdad3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
+(* $Id: cases.ml 10071 2007-08-10 15:34:41Z herbelin $ *)
 
 open Util
 open Names
@@ -1021,18 +1021,18 @@ let abstract_predicate env sigma indf cur tms = function
       (* Depending on whether the predicate is dependent or not, and has real
          args or not, we lift it to make room for [sign] *)
       (* Even if not intrinsically dep, we move the predicate into a dep one *)
-      let sign,k =
+      let sign,q =
         if names = [] & n <> 1 then
           (* Real args were not considered *)
           (if dep<>Anonymous then
-            ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1)
+            (let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign)
           else
-            (sign,n))
+            sign),n
         else
           (* Real args are OK *)
-          (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,
-           if dep<>Anonymous then 0 else 1) in
-      let pred = lift_predicate k pred in
+          (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,1) in
+      let q,k = if dep <> Anonymous then (q-1,2) else (q,1) in
+      let pred = liftn_predicate q k pred in
       let pred = extract_predicate [] (pred,tms) in
       (true, it_mkLambda_or_LetIn_name env pred sign)
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 4a2e5ee3..29ec7904 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: detyping.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
 
 open Pp
 open Util
@@ -241,7 +241,9 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
   | [] -> [[],rhs]
   | na::nal ->
     match kind_of_term c with
-    | Case (ci,_,c,cl) when c = mkRel (list_index na (snd e)) ->
+    | Case (ci,p,c,cl) when c = mkRel (list_index na (snd e)) 
+	& (* don't contract if p dependent *)
+	computable p (ci.ci_pp_info.ind_nargs) ->
 	let clauses = build_tree na isgoal e ci cl in
 	List.flatten
           (List.map (fun (pat,rhs) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 92617820..64e9ebec 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 9762 2007-04-13 12:46:50Z herbelin $ *)
+(* $Id: tacred.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
 
 open Pp
 open Util
@@ -358,12 +358,11 @@ let reduce_fix_use_function f whfun fix stack =
 	       Reduced (contract_fix_use_function f fix,stack')
 	   | _ -> NotReducible)
 
-let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
+let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j = match f j with
     | None -> mkCoFix(j,typedbodies)
     | Some c -> c in
-(*    match List.nth names j with Name id -> f id | _ -> assert false in*)
   let subbodies = list_tabulate make_Fi nbodies in
   substl (List.rev subbodies) bodies.(bodynum)
 
@@ -372,19 +371,27 @@ let reduce_mind_case_use_function func env mia =
     | Construct(ind_sp,i) ->
 	let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
 	applist (mia.mlf.(i-1), real_cargs)
-    | CoFix (_,(names,_,_) as cofix) ->
-	let build_fix_name i =
-	  match names.(i) with 
-	    | Name id ->
-                if isConst func then
-		  let (mp,dp,_) = repr_con (destConst func) in
-		  let kn = make_con mp dp (label_of_id id) in
-		  (match constant_opt_value env kn with
-		    | None -> None
-		    | Some _ -> Some (mkConst kn))
-                else None
-	    | Anonymous -> None in 
-	let cofix_def = contract_cofix_use_function build_fix_name cofix in
+    | CoFix (bodynum,(names,_,_) as cofix) ->
+	let build_cofix_name =
+	  if isConst func then
+	    let (mp,dp,_) = repr_con (destConst func) in
+	    fun i ->
+	      if i = bodynum then Some func
+	      else match names.(i) with
+                | Anonymous -> None
+		| Name id ->
+		    (* In case of a call to another component of a block of 
+		       mutual inductive, try to reuse the global name if
+		       the block was indeed initially built as a global 
+		       definition *)
+		    let kn = make_con mp dp (label_of_id id) in
+		    try match constant_opt_value env kn with
+		      | None -> None
+		      | Some _ -> Some (mkConst kn)
+		    with Not_found -> None
+	  else
+	    fun _ -> None in
+	let cofix_def = contract_cofix_use_function build_cofix_name cofix in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false