- Fixing bug 1703 ("intros until n" falls back on the variable name when

  the latter is bound to a var which is not a quantified one - this led
  to remove a line marked "temporary compatibility" ... ; made a distinction
  between quantified hypothesis as for "intros until" and binding names as
  in "apply with"; in both cases, we now expect that a identifier not used 
  as a variable, as in "apply f_equal with f:=g" where "f" is a true binder
  name in f_equal, must not be used as a variable elsewhere [see
  corresponding change in Ints/Tactic.v])
- Fixing bug 1643 (bug in the algorithm used to possibly reuse a
  global name in the recursive calls of a coinductive term)
- Fixing bug 1699 (bug in contracting nested patterns at printing time
  when the return clause of the subpatterns is dependent)
- Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic)
- Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 24 insertions, 12 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 21ea677579..049c936415 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -242,7 +242,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 fa62c44657..d276d2dd79 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -355,9 +355,9 @@ 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 names.(j) with
+  let make_Fi j = match f j with
     | None -> mkCoFix(j,typedbodies)
     | Some c -> c in
   let subbodies = list_tabulate make_Fi nbodies in
@@ -368,15 +368,25 @@ 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 cofix ->
-	let build_cofix_name = function
-	  | Name id when isConst func ->
-	      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))
-	  | _ -> None 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
+		| 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