Correction de bugs:

- evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un
  terme applicatif au moment de tester f u1 .. un = g v1 .. vn au
  premier ordre : on revient sur l'algo tel qu'il était avant le
  commit 11187.
- Bug #1887 (format récursif cassé à cause de la vérification des idents).
- Nouveau choix de formattage du message "Tactic Failure".
- Nettoyage vocabulaire "match context" -> "match goal" au passage.


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

15 files changed, 61 insertions, 52 deletions

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index bf1cf5e7b..203bc9e3d 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -268,7 +268,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
 	     igtal
 	     acc)
     | TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet"
-    | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
+    | TacMatchGoal (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
     | TacFun tacfa -> depends_of_tac_fun_ast tacfa acc
     | TacArg tacarg -> depends_of_tac_arg tacarg acc
   and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 716f6da3b..e368ff637 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -830,11 +830,11 @@ and xlate_tactic =
                          | [] -> assert false
                          | fst::others ->
                              CT_match_tac_rules(fst, others))
-   | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
-   | TacMatchContext (false,false,rule1::rules) ->
+   | TacMatchGoal (_,_,[]) | TacMatchGoal (true,_,_) -> failwith ""
+   | TacMatchGoal (false,false,rule1::rules) ->
          CT_match_context(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacMatchContext (false,true,rule1::rules) ->
+   | TacMatchGoal (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
    | TacLetIn (false, l, t) ->
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index 29feab5ca..531ab3ca5 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -494,7 +494,7 @@ Qed.
  Proof. intros;mrewrite. Qed.
 
  Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y.
- Proof. 
+ Proof.
   intros;mrewrite. 
   repeat rewrite (ARth.(ARmul_comm) z);sreflexivity.
  Qed.
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index d9bc8038b..f869dc8e8 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -72,10 +72,10 @@ GEXTEND Gram
       | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
     | "1" RIGHTA
       [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
-          TacMatchContext (b,false,mrl)
+          TacMatchGoal (b,false,mrl)
       | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
-          TacMatchContext (b,true,mrl)
+          TacMatchGoal (b,true,mrl)
       |	b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
           TacMatch (b,c,mrl)
       | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 8d1dbf875..933667ce3 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -899,7 +899,7 @@ let rec pr_tac inherited tac =
 	lrul
         ++ fnl() ++ str "end"),
       lmatch
-  | TacMatchContext (lz,lr,lrul) ->
+  | TacMatchGoal (lz,lr,lrul) ->
       hov 0 (pr_lazy lz ++ 
 	str (if lr then "match reverse goal with" else "match goal with")
 	++ prlist
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 56afbc9be..113e88cd3 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -470,8 +470,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
         $mlexpr_of_bool lz$
         $mlexpr_of_tactic t$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
-  | Tacexpr.TacMatchContext (lz,lr,l) ->
-      <:expr< Tacexpr.TacMatchContext 
+  | Tacexpr.TacMatchGoal (lz,lr,l) ->
+      <:expr< Tacexpr.TacMatchGoal 
         $mlexpr_of_bool lz$
         $mlexpr_of_bool lr$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4d5710860..667ea458c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -273,11 +273,10 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f1 i =
-	  if l1 <> [] && l2 <> [] then
-            ise_list2 i (fun i -> evar_conv_x env i CONV)
-	      (flex1::l1) (flex2::l2)
+	  if flex1 = flex2 then
+	    ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
 	  else
-	    (i,false)
+	     (i,false)
 	and f2 i =
 	  (try conv_record env i
              (try check_conv_record appr1 appr2
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 34ddbb189..29d7a7bb1 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -253,7 +253,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
-  | TacMatchContext of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
   | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a2e6587ee..9c3ffd292 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -657,17 +657,17 @@ let extend_values_with_bindings (ln,lm) lfun =
      binding of the same name exists *)
   lmatch@lfun@lnames
 
-(* Reads the hypotheses of a Match Context rule *)
-let rec intern_match_context_hyps sigma env lfun = function
+(* Reads the hypotheses of a "match goal" rule *)
+let rec intern_match_goal_hyps sigma env lfun = function
   | (Hyp ((_,na) as locna,mp))::tl ->
       let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in
-      let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in
+      let lfun, metas2, hyps = intern_match_goal_hyps sigma env lfun tl in
       let lfun' = name_cons na (Option.List.cons ido lfun) in
       lfun', metas1@metas2, Hyp (locna,pat)::hyps
   | (Def ((_,na) as locna,mv,mp))::tl ->
       let ido, metas1, patv = intern_pattern sigma env ~as_type:false lfun mv in
       let ido', metas2, patt = intern_pattern sigma env ~as_type:true lfun mp in
-      let lfun, metas3, hyps = intern_match_context_hyps sigma env lfun tl in
+      let lfun, metas3, hyps = intern_match_goal_hyps sigma env lfun tl in
       let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
       lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
   | [] -> lfun, [], []
@@ -835,8 +835,8 @@ and intern_tactic_seq ist = function
       let l = List.map (fun (n,b) -> 
 	  (n,intern_tacarg !strict_check (if isrec then ist' else ist) b)) l in
       ist.ltacvars, TacLetIn (isrec,l,intern_tactic ist' u)
-  | TacMatchContext (lz,lr,lmr) ->
-      ist.ltacvars, TacMatchContext(lz,lr, intern_match_rule ist lmr)
+  | TacMatchGoal (lz,lr,lmr) ->
+      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule ist lmr)
   | TacMatch (lz,c,lmr) ->
       ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr)
   | TacId l -> ist.ltacvars, TacId (intern_message ist l)
@@ -912,7 +912,7 @@ and intern_match_rule ist = function
       All (intern_tactic ist tc) :: (intern_match_rule ist tl)
   | (Pat (rl,mp,tc))::tl ->
       let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
-      let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in
+      let lfun',metas1,hyps = intern_match_goal_hyps sigma env lfun rl in
       let ido,metas2,pat = intern_pattern sigma env lfun mp in
       let metas = list_uniquize (metas1@metas2) in
       let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
@@ -1012,27 +1012,27 @@ let read_pattern lfun = function
 (* Reads the hypotheses of a Match Context rule *)
 let cons_and_check_name id l =
   if List.mem id l then
-    user_err_loc (dloc,"read_match_context_hyps",
+    user_err_loc (dloc,"read_match_goal_hyps",
       strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^
       " used twice in the same pattern."))
   else id::l
 
-let rec read_match_context_hyps lfun lidh = function
+let rec read_match_goal_hyps lfun lidh = function
   | (Hyp ((loc,na) as locna,mp))::tl ->
       let lidh' = name_fold cons_and_check_name na lidh in
       Hyp (locna,read_pattern lfun mp)::
-	(read_match_context_hyps lfun lidh' tl)
+	(read_match_goal_hyps lfun lidh' tl)
   | (Def ((loc,na) as locna,mv,mp))::tl ->
       let lidh' = name_fold cons_and_check_name na lidh in
       Def (locna,read_pattern lfun mv, read_pattern lfun mp)::
-	(read_match_context_hyps lfun lidh' tl)
+	(read_match_goal_hyps lfun lidh' tl)
   | [] -> []
 
 (* Reads the rules of a Match Context or a Match *)
 let rec read_match_rule lfun = function
   | (All tc)::tl -> (All tc)::(read_match_rule lfun tl)
   | (Pat (rl,mp,tc))::tl ->
-      Pat (read_match_context_hyps lfun [] rl, read_pattern lfun mp,tc)
+      Pat (read_match_goal_hyps lfun [] rl, read_pattern lfun mp,tc)
       :: read_match_rule lfun tl
   | [] -> []
 
@@ -1724,7 +1724,7 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
   | TacFun (it,body) -> VFun (ist.trace,ist.lfun,it,body)
   | TacLetIn (true,l,u) -> interp_letrec ist gl l u
   | TacLetIn (false,l,u) -> interp_letin ist gl l u
-  | TacMatchContext (lz,lr,lmr) -> interp_match_context ist gl lz lr lmr 
+  | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist gl lz lr lmr 
   | TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr
   | TacArg a -> interp_tacarg ist gl a
   (* Delayed evaluation *)
@@ -1746,7 +1746,7 @@ and eval_tactic ist = function
 	(* catch error in the evaluation *)
 	catch_error ((loc,call)::ist.trace) tac gl
   | TacFun _ | TacLetIn _ -> assert false
-  | TacMatchContext _ | TacMatch _ -> assert false
+  | TacMatchGoal _ | TacMatch _ -> assert false
   | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
   | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
@@ -1890,7 +1890,7 @@ and interp_letin ist gl llc u =
   val_interp ist gl u
 
 (* Interprets the Match Context expressions *)
-and interp_match_context ist goal lz lr lmr =
+and interp_match_goal ist goal lz lr lmr =
   let hyps = pf_hyps goal in
   let hyps = if lr then List.rev hyps else hyps in
   let concl = pf_concl goal in
@@ -1902,7 +1902,7 @@ and interp_match_context ist goal lz lr lmr =
       try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
       with e when is_match_catchable e -> match_next_pattern find_next' () in
     match_next_pattern (fun () -> match_subterm_gen app c csr) () in
-  let rec apply_match_context ist env goal nrs lex lpt = 
+  let rec apply_match_goal ist env goal nrs lex lpt = 
     begin
       if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
       match lpt with
@@ -1911,7 +1911,7 @@ and interp_match_context ist goal lz lr lmr =
               db_mc_pattern_success ist.debug;
               try eval_with_fail ist lz goal t
               with e when is_match_catchable e ->
-		apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+		apply_match_goal ist env goal (nrs+1) (List.tl lex) tl
 	    end
 	| (Pat (mhyps,mgoal,mt))::tl ->
             let mhyps = List.rev mhyps (* Sens naturel *) in
@@ -1926,20 +1926,20 @@ and interp_match_context ist goal lz lr lmr =
 		       | PatternMatchingFailure -> db_matching_failure ist.debug
 		       | Eval_fail s -> db_eval_failure ist.debug s
 		       | _ -> db_logic_failure ist.debug e);
-		     apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
+		     apply_match_goal ist env goal (nrs+1) (List.tl lex) tl)
 	     | Subterm (b,id,mg) ->
 		 (try apply_goal_sub b ist (id,mg) concl mt mhyps hyps
 		   with
 		     | PatternMatchingFailure ->
-			 apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
+			 apply_match_goal ist env goal (nrs+1) (List.tl lex) tl))
 	| _ ->
-	    errorlabstrm "Tacinterp.apply_match_context"
+	    errorlabstrm "Tacinterp.apply_match_goal"
               (v 0 (str "No matching clauses for match goal" ++
 		      (if ist.debug=DebugOff then
 			 fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
 		       else mt()) ++ str"."))
     end in
-    apply_match_context ist env goal 0 lmr
+    apply_match_goal ist env goal 0 lmr
       (read_match_rule (fst (constr_list ist env)) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
@@ -2498,13 +2498,13 @@ let subst_match_pattern subst = function
   | Subterm (b,ido,pc) -> Subterm (b,ido,subst_pattern subst pc)
   | Term pc -> Term (subst_pattern subst pc)
 
-let rec subst_match_context_hyps subst = function
+let rec subst_match_goal_hyps subst = function
   | Hyp (locs,mp) :: tl ->
       Hyp (locs,subst_match_pattern subst mp)
-      :: subst_match_context_hyps subst tl
+      :: subst_match_goal_hyps subst tl
   | Def (locs,mv,mp) :: tl ->
       Def (locs,subst_match_pattern subst mv, subst_match_pattern subst mp)
-      :: subst_match_context_hyps subst tl
+      :: subst_match_goal_hyps subst tl
   | [] -> []
 
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
@@ -2609,8 +2609,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacLetIn (r,l,u) ->
       let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in
       TacLetIn (r,l,subst_tactic subst u)
-  | TacMatchContext (lz,lr,lmr) ->
-      TacMatchContext(lz,lr, subst_match_rule subst lmr)
+  | TacMatchGoal (lz,lr,lmr) ->
+      TacMatchGoal(lz,lr, subst_match_rule subst lmr)
   | TacMatch (lz,c,lmr) ->
       TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr)
   | TacId _ | TacFail _ as x -> x
@@ -2657,7 +2657,7 @@ and subst_match_rule subst = function
   | (All tc)::tl ->
       (All (subst_tactic subst tc))::(subst_match_rule subst tl)
   | (Pat (rl,mp,tc))::tl ->
-      let hyps = subst_match_context_hyps subst rl in
+      let hyps = subst_match_goal_hyps subst rl in
       let pat = subst_match_pattern subst mp in
       Pat (hyps,pat,subst_tactic subst tc)
       ::(subst_match_rule subst tl)
diff --git a/test-suite/output/Match_subterm.out b/test-suite/output/Match_subterm.out
new file mode 100644
index 000000000..951a98db0
--- /dev/null
+++ b/test-suite/output/Match_subterm.out
@@ -0,0 +1,8 @@
+(0 = 1)
+eq
+nat
+0
+1
+S
+0
+2
diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v
new file mode 100644
index 000000000..2c44b1879
--- /dev/null
+++ b/test-suite/output/Match_subterm.v
@@ -0,0 +1,6 @@
+Goal 0 = 1.
+match goal with
+| |- context [?v] =>
+  idtac v ; fail
+| _ => idtac 2
+end.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 3bc9c7f9e..082cbfbe1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -198,11 +198,6 @@ Goal forall x : nat, F1 x -> G1 x.
 refine (fun x H => proj2 (_ x H) _).
 Abort.
 
-(* First-order unification between beta-redex (is it useful ?) *)
-
-Check fun (y: (forall x:((fun y:Type => bool) nat), True))
-          (z: (fun z:Type => bool) _) => y z.
-
 (* Remark: the following example does not succeed any longer in 8.2 because,
    the algorithm is more general and does exclude a solution that it should
    exclude for typing reason. Handling of types and backtracking is still to
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index f0a17d7a4..705fb3bdf 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -115,7 +115,7 @@ lazymatch T with
     evar (a : t); pose proof (H a) as H1; unfold a in H1;
     clear a; clear H; rename H1 into H; find_equiv H
 | ?A <-> ?B => idtac
-| _ => fail "The given statement does not seem to end with an equivalence."
+| _ => fail "The given statement does not seem to end with an equivalence"
 end.
 
 Ltac bapply lemma todo :=
@@ -141,7 +141,7 @@ t;
 match goal with
 | H : _ |- _ => solve [inversion H]
 | _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split]
-| _ => fail 1 "Cannot solve this goal."
+| _ => fail 1 "Cannot solve this goal"
 end.
 
 (** A tactic to document or check what is proved at some point of a script *)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 488c39834..f34621216 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -105,8 +105,9 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
 	       str "No constant of this name:" ++ spc () ++ 
                Libnames.pr_qualid q ++ str ".")
   | Refiner.FailError (i,s) ->
-      hov 0 (str "Error: Tactic failure:" ++ s ++
-             if i=0 then mt () else str " (level " ++ int i ++ str").")
+      hov 0 (str "Error: Tactic failure" ++ 
+                (if s <> mt() then str ":" ++ s else mt ()) ++
+                if i=0 then str "." else str " (level " ++ int i ++ str").")
   | Stdpp.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 50d30cda7..a14d42074 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -485,7 +485,7 @@ let make_hunks etyps symbols from =
 let error_format () = error "The format does not match the notation."
 
 let rec split_format_at_ldots hd = function
-  | UnpTerminal s :: fmt when id_of_string s = ldots_var -> List.rev hd, fmt
+  | UnpTerminal s :: fmt when s = string_of_id ldots_var -> List.rev hd, fmt
   | u :: fmt -> 
       check_no_ldots_in_box u;
       split_format_at_ldots (u::hd) fmt