- 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

9 files changed, 117 insertions, 32 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 763261bfd5..32d9f107cf 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -942,6 +942,8 @@ let rec raw_of_pat env = function
   | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
       let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
       RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
+  | PCase (_,PMeta None,tm,[||]) ->
+      RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[])
   | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
       let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
       let brns = Array.to_list cstr_nargs in
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
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 77d9c265f4..884afebb9a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -450,9 +450,16 @@ let rec intern_intro_pattern lf ist = function
 and intern_case_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
 
-let intern_quantified_hypothesis ist x =
-  (* We use identifier both for variables and quantified hyps (no way to
-     statically check the existence of a quantified hyp); thus nothing to do *)
+let intern_quantified_hypothesis ist = function
+  | AnonHyp n -> AnonHyp n
+  | NamedHyp id ->
+      (* Uncomment to disallow "intros until n" in ltac when n is not bound *)
+      NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*))
+      
+let intern_binding_name ist x =
+  (* We use identifier both for variables and binding names *)
+  (* Todo: consider the body of the lemma to which the binding refer 
+     and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
 let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
@@ -467,7 +474,7 @@ let intern_type = intern_constr_gen true
 
 (* Globalize bindings *)
 let intern_binding ist (loc,b,c) =
-  (loc,intern_quantified_hypothesis ist b,intern_constr ist c)
+  (loc,intern_binding_name ist b,intern_constr ist c)
 
 let intern_bindings ist = function
   | NoBindings -> NoBindings
@@ -1518,9 +1525,16 @@ let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
-      with Not_found 
-      | Stdpp.Exc_located (_, UserError _) | UserError _ (*Compat provisoire*)
-   -> NamedHyp id
+      with Not_found -> NamedHyp id
+
+let interp_binding_name ist = function
+  | AnonHyp n -> AnonHyp n
+  | NamedHyp id ->
+      (* If a name is bound, it has to be a quantified hypothesis *)
+      (* user has to use other names for variables if these ones clash with *)
+      (* a name intented to be used as a (non-variable) identifier *)
+      try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
+      with Not_found -> NamedHyp id
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
@@ -1548,7 +1562,7 @@ let interp_induction_arg ist gl = function
 	(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))))
 
 let interp_binding ist gl (loc,b,c) =
-  (loc,interp_quantified_hypothesis ist b,pf_interp_open_constr false ist gl c)
+  (loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c)
 
 let interp_bindings ist gl = function
 | NoBindings -> NoBindings
@@ -1803,7 +1817,7 @@ and interp_match_context ist g lz lr lmr =
 	    errorlabstrm "Tacinterp.apply_match_context"
               (v 0 (str "No matching clauses for match goal" ++
 		      (if ist.debug=DebugOff then
-			 fnl() ++ str "(use \"Debug On\" for more info)"
+			 fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
 		       else mt())))
     end in
   let env = pf_env g in
@@ -2405,7 +2419,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
   | TacCut c -> TacCut (subst_rawconstr subst c)
-  | TacAssert (b,na,c) -> TacAssert (b,na,subst_rawconstr subst c)
+  | TacAssert (b,na,c) ->
+      TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c)
   | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
   | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
diff --git a/test-suite/bugs/closed/shouldfail/1703.v b/test-suite/bugs/closed/shouldfail/1703.v
new file mode 100644
index 0000000000..6b5198cc03
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/1703.v
@@ -0,0 +1,7 @@
+(* Check correct binding of intros until used in Ltac *)
+
+Ltac intros_until n := intros until n.
+
+Goal forall i j m n : nat, i = 0 /\ j = 0 /\ m = 0 /\ n = 0.
+intro i.
+intros until i.
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v
new file mode 100644
index 0000000000..6ecbc810b7
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1643.v
@@ -0,0 +1,20 @@
+(* Check some aspects of that the algorithm used to possibly reuse a
+   global name in the recursive calls (coinductive case) *)
+
+CoInductive Str : Set := Cons (h:nat) (t:Str).
+
+Definition decomp_func (s:Str) :=
+   match s with
+   | Cons h t => Cons h t
+   end.
+
+Theorem decomp s: s = decomp_func s.
+Proof.
+intros s.
+case s; simpl; reflexivity.
+Qed.
+
+Definition zeros := (cofix z : Str := Cons 0 z).
+Lemma zeros_rw : zeros = Cons 0 zeros.
+rewrite (decomp zeros).
+simpl.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index a3033e94fc..3c440b9d02 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -7,3 +7,16 @@ fix F (t : t) : P t :=
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
+proj = 
+fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
+match eq_nat_dec x y with
+| left eqprf =>
+    match eqprf in (_ = z) return (P z) with
+    | refl_equal => def
+    end
+| right _ => prf
+end
+     : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
+
+
+Argument scopes are [nat_scope nat_scope _ _ _]
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 452d360362..56d5cfb4e7 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -4,3 +4,19 @@ Inductive t : Set :=
     k : let x := t in x -> x.
 
 Print t_rect.
+
+(* Do not contract nested patterns with dependent return type *)
+(* see bug #1699 *)
+
+Require Import Arith.
+
+Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y :=
+  match eq_nat_dec x y return P y with
+  | left eqprf => 
+    match eqprf in (_ = z) return (P z) with
+    | refl_equal => def
+    end
+  | _ => prf
+ end.
+
+Print proj.
diff --git a/theories/Ints/Tactic.v b/theories/Ints/Tactic.v
index a1654da687..08daffa551 100644
--- a/theories/Ints/Tactic.v
+++ b/theories/Ints/Tactic.v
@@ -65,16 +65,16 @@ Ltac case_eq name :=
 
 Ltac eq_tac := 
  match goal with
-      |-  (?f _ = ?f _) => apply f_equal with (f := f)
- |     |-  (?f ?X _ = ?f  ?X _) => apply f_equal with (f := f  X)
- |     |-  (?f _ _ = ?f  _ _) => apply f_equal2 with (f := f)
- |     |-  (?f ?X ?Y _ = ?f ?X ?Y _) => apply f_equal with (f := f X Y)
- |     |-  (?f ?X _ _ = ?f ?X _ _) => apply f_equal2 with (f := f X)
- |     |-  (?f _ _ _ = ?f _ _ _) => apply f_equal3 with (f := f)
- |     |-  (?f ?X ?Y ?Z _ = ?f ?X ?Y ?Z _) => apply f_equal with (f := f X Y Z)
- |     |-  (?f ?X ?Y _ _ = ?f ?X ?Y _ _) => apply f_equal2 with (f := f X Y)
- |     |-  (?f ?X _ _ _ = ?f ?X _ _ _) => apply f_equal3 with (f := f X)
- |     |-  (?f _ _ _ _ _ = ?f _ _ _ _) => apply f_equal4 with (f := f)
+       |-  (?g _ = ?g _) => apply f_equal with (f := g)
+ |     |-  (?g ?X _ = ?g  ?X _) => apply f_equal with (f := g  X)
+ |     |-  (?g _ _ = ?g  _ _) => apply f_equal2 with (f := g)
+ |     |-  (?g ?X ?Y _ = ?g ?X ?Y _) => apply f_equal with (f := g X Y)
+ |     |-  (?g ?X _ _ = ?g ?X _ _) => apply f_equal2 with (f := g X)
+ |     |-  (?g _ _ _ = ?g _ _ _) => apply f_equal3 with (f := g)
+ |     |-  (?g ?X ?Y ?Z _ = ?g ?X ?Y ?Z _) => apply f_equal with (f := g X Y Z)
+ |     |-  (?g ?X ?Y _ _ = ?g ?X ?Y _ _) => apply f_equal2 with (f := g X Y)
+ |     |-  (?g ?X _ _ _ = ?g ?X _ _ _) => apply f_equal3 with (f := g X)
+ |     |-  (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g)
  end.
 
 (**************************************