Modification rapide du message d'erreur lorsqu'un _ ne peut être

effacé dans un intro-pattern (suggéré par ssreflect).



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

3 files changed, 28 insertions, 13 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6edc723cf2..4e06fffb74 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -376,7 +376,7 @@ let rewrite_equations_gene othin neqns ba gl =
      Some thin: the equations are rewritten, and cleared if thin is true *)
 
 let rec get_names allow_conj = function
-  | IntroWildcard ->
+  | IntroWildcard _ ->
       error "Discarding pattern not allowed for inversion equations."
   | IntroAnonymous ->
       error "Anonymous pattern not allowed for inversion equations."
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f81f15d891..1af19868a3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -98,7 +98,9 @@ let catch_error loc tac g =
   try tac g
   with e when loc <> dummy_loc ->
     match e with
-      |	Stdpp.Exc_located (_,e) -> raise (Stdpp.Exc_located (loc,e))
+      |	Stdpp.Exc_located (loc',e') ->
+	  if loc' = dummy_loc then raise (Stdpp.Exc_located (loc,e'))
+	  else raise e
       |	e -> raise (Stdpp.Exc_located (loc,e))
 
 (* Signature for interpretation: val_interp and interpretation functions *)
@@ -488,7 +490,7 @@ let rec intern_intro_pattern lf ist = function
       IntroOrAndPattern (intern_case_intro_pattern lf ist l)
   | IntroIdentifier id ->
       IntroIdentifier (intern_ident lf ist id)
-  | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
+  | IntroWildcard _ | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
 
 and intern_case_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
@@ -1364,7 +1366,7 @@ let rec intropattern_ids = function
   | IntroIdentifier id -> [id]
   | IntroOrAndPattern ll -> 
       List.flatten (List.map intropattern_ids (List.flatten ll))
-  | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> []
+  | IntroWildcard _ | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> []
 
 let rec extract_ids ids = function
   | (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
@@ -1638,7 +1640,7 @@ let rec interp_message_nl ist = function
 let rec interp_intro_pattern ist gl = function
   | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist gl l)
   | IntroIdentifier id -> interp_intro_pattern_var ist (pf_env gl) id
-  | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
+  | IntroWildcard _ | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
 
 and interp_case_intro_pattern ist gl =
   List.map (List.map (interp_intro_pattern ist gl))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1fdd4c16fe..8c84b40d15 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -882,11 +882,24 @@ let (assumption : tactic) = fun gl ->
  * subsequently used in other hypotheses or in the conclusion of the  
  * goal. *)                                                               
 
-let clear ids gl = (* avant seul dyn_clear n'echouait pas en [] *)
-  if ids=[] then tclIDTAC gl else with_check (thin ids) gl
+let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
+  if ids=[] then tclIDTAC else thin ids
 
 let clear_body = thin_body
 
+let clear_wildcards ids =
+  tclMAP (fun (loc,id) gl ->
+    try with_check (Tacmach.thin_no_check [id]) gl
+    with OccurHypInSimpleClause (id,ido) ->
+      (* Intercept standard [thin] error message *)
+      match ido with
+      | None ->
+	user_err_loc (loc,"",str "_ is used in conclusion.")
+      | Some id -> 
+	user_err_loc
+	  (loc,"",str "_ is used in hypothesis " ++ pr_id id ++ str "."))
+    ids
+
 (*   Takes a list of booleans, and introduces all the variables 
  *  quantified in the goal which are associated with a value
  *  true  in the boolean list. *)
@@ -1056,7 +1069,7 @@ let clear_if_atomic l2r id gl =
 let rec explicit_intro_names = function
 | IntroIdentifier id :: l ->
     id :: explicit_intro_names l
-| (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _) :: l ->
+| (IntroWildcard _ | IntroAnonymous | IntroFresh _ | IntroRewrite _) :: l ->
     explicit_intro_names l
 | IntroOrAndPattern ll :: l' -> 
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
@@ -1068,13 +1081,13 @@ let rec explicit_intro_names = function
      dependency order (see bug #1000); we use fresh names, not used in
      the tactic, for the hyps to clear *)
 let rec intros_patterns avoid thin destopt = function
-  | IntroWildcard :: l ->
+  | IntroWildcard loc :: l ->
       tclTHEN 
         (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) None true)
         (onLastHyp (fun id ->
 	  tclORELSE
 	    (tclTHEN (clear [id]) (intros_patterns avoid thin destopt l))
-	    (intros_patterns avoid (id::thin) destopt l)))
+	    (intros_patterns avoid ((loc,id)::thin) destopt l)))
   | IntroIdentifier id :: l ->
       tclTHEN
         (intro_gen (IntroMustBe id) destopt true)
@@ -1100,7 +1113,7 @@ let rec intros_patterns avoid thin destopt = function
 	      allClauses;
 	    clear_if_atomic l2r id;
 	    intros_patterns avoid thin destopt l ]))
-  | [] -> clear thin
+  | [] -> clear_wildcards thin
 
 let intros_pattern = intros_patterns [] []
 
@@ -1122,7 +1135,7 @@ let make_id s = fresh_id [] (match s with Prop _ -> hid | Type _ -> xid)
 let prepare_intros s ipat gl = match ipat with
   | IntroAnonymous -> make_id s gl, tclIDTAC
   | IntroFresh id -> fresh_id [] id gl, tclIDTAC
-  | IntroWildcard -> let id = make_id s gl in id, thin [id]
+  | IntroWildcard loc -> let id = make_id s gl in id, clear_wildcards [loc,id]
   | IntroIdentifier id -> id, tclIDTAC
   | IntroRewrite l2r -> 
       let id = make_id s gl in
@@ -1456,7 +1469,7 @@ let rec first_name_buggy = function
   | IntroOrAndPattern [] -> None
   | IntroOrAndPattern ([]::l) -> first_name_buggy (IntroOrAndPattern l)
   | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p
-  | IntroWildcard -> None
+  | IntroWildcard _ -> None
   | IntroRewrite _ -> None
   | IntroIdentifier id -> Some id
   | IntroAnonymous | IntroFresh _ -> assert false