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

11 files changed, 60 insertions, 30 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8b805cc26..2e4ff80bb 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -625,7 +625,7 @@ let rec xlate_intro_pattern =
 	   (fun l ->
 	      CT_intro_patt_list(List.map xlate_intro_pattern l))
 	   ll)
-  | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
+  | IntroWildcard _ -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
   | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
   | IntroFresh _ -> xlate_error "TODO: IntroFresh"
diff --git a/interp/genarg.ml b/interp/genarg.ml
index ac45bfe8d..b371582a1 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -76,7 +76,7 @@ let exists_argtype s = List.mem s !dyntab
 
 type intro_pattern_expr =
   | IntroOrAndPattern of case_intro_pattern_expr
-  | IntroWildcard
+  | IntroWildcard of loc
   | IntroIdentifier of identifier
   | IntroAnonymous
   | IntroRewrite of bool
@@ -85,7 +85,7 @@ and case_intro_pattern_expr = intro_pattern_expr list list
 
 let rec pr_intro_pattern = function
   | IntroOrAndPattern pll -> pr_case_intro_pattern pll
-  | IntroWildcard -> str "_"
+  | IntroWildcard _ -> str "_"
   | IntroIdentifier id -> pr_id id
   | IntroAnonymous -> str "?"
   | IntroRewrite true -> str "->"
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 977308218..da0371899 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -33,7 +33,7 @@ type 'a with_ebindings = 'a * open_constr bindings
 
 type intro_pattern_expr =
   | IntroOrAndPattern of case_intro_pattern_expr
-  | IntroWildcard
+  | IntroWildcard of loc
   | IntroIdentifier of identifier
   | IntroAnonymous
   | IntroRewrite of bool
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a1fd1649e..092dc9f88 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -251,7 +251,7 @@ GEXTEND Gram
 	    | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
 	    | t::q -> IntroOrAndPattern [[t;pairify q]]
 	  in pairify (si::tc)
-      | "_" -> IntroWildcard
+      | "_" -> IntroWildcard loc
       | prefix = pattern_ident -> IntroFresh prefix
       | "?" -> IntroAnonymous
       | id = ident -> IntroIdentifier id
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6bd795ed5..66a74ad16 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -62,12 +62,16 @@ let mlexpr_of_reference = function
   | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
   | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
 
+let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
+
+let mlexpr_of_loc loc = <:expr< $dloc$ >>
+
 let mlexpr_of_by_notation f = function
   | Genarg.AN x -> <:expr< Genarg.AN $f x$ >>
   | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >>
 
 let mlexpr_of_intro_pattern = function
-  | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
+  | Genarg.IntroWildcard loc -> <:expr< Genarg.IntroWildcard $mlexpr_of_loc loc$ >>
   | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
   | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >>
   | Genarg.IntroIdentifier id ->
@@ -85,10 +89,6 @@ let mlexpr_of_quantified_hypothesis = function
   | Rawterm.AnonHyp n -> <:expr< Rawterm.AnonHyp $mlexpr_of_int n$ >>
   | Rawterm.NamedHyp id ->  <:expr< Rawterm.NamedHyp $mlexpr_of_ident id$ >>
 
-let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
-
-let mlexpr_of_loc loc = <:expr< $dloc$ >>
-
 let mlexpr_of_or_var f = function
   | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >>
   | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2f2665bbc..f0c020908 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -437,12 +437,14 @@ let rec check_and_clear_in_constr evdref c ids hist =
 
       | _ -> map_constr (fun c -> check_and_clear_in_constr evdref c ids hist) c
 
+exception OccurHypInSimpleClause of identifier * identifier option
+
 let clear_hyps_in_evi evdref hyps concl ids =
   (* clear_evar_hyps erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occuring in evi *)
   let nconcl = try check_and_clear_in_constr evdref concl ids EvkSet.empty
-    with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in
+    with Dependency_error id' -> raise (OccurHypInSimpleClause (id',None)) in
   let (nhyps,_) = 
     let check_context (id,ob,c) = 
       try
@@ -451,9 +453,7 @@ let clear_hyps_in_evi evdref hyps concl ids =
 	    None -> None
 	  | Some b -> Some (check_and_clear_in_constr evdref b ids EvkSet.empty)),
 	check_and_clear_in_constr evdref c ids EvkSet.empty)
-      with Dependency_error id' ->
-	errorlabstrm "" (pr_id id' ++ strbrk " is used in hypothesis "
-					   ++ pr_id id ++ str ".")
+      with Dependency_error id' -> raise (OccurHypInSimpleClause (id',Some id))
     in
     let check_value vk =
       match !vk with
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 27e964b6a..c48c97910 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -172,7 +172,11 @@ val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
 
 
-(**********************************)
-(* Removing hyps in evars'context *)
+(*********************************************************************)
+(* Removing hyps in evars'context;                                   *)
+(* raise OccurHypInSimpleClause if the removal breaks dependencies   *)
+
+exception OccurHypInSimpleClause of identifier * identifier option
+
 val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types ->
   identifier list -> named_context_val * types
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7fd7aabe4..8e3e48d4f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -8,6 +8,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
 open Nameops
@@ -226,11 +227,21 @@ let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t)
 let refine c           = with_check (refine_no_check c)
 let convert_concl d sty = with_check (convert_concl_no_check d sty)
 let convert_hyp d      = with_check (convert_hyp_no_check d)
-let thin l             = with_check (thin_no_check l)
 let thin_body c        = with_check (thin_body_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
 let rename_hyp l       = with_check (rename_hyp_no_check l)
 
+let thin l gl = 
+  try with_check (thin_no_check l) gl
+  with Evarutil.OccurHypInSimpleClause (id,ido) ->
+    match ido with
+    | None ->
+	errorlabstrm "" (pr_id id ++ str " is used in conclusion.")
+    | Some id' -> 
+	errorlabstrm "" 
+	 (pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str ".")
+
+
 (* Pretty-printers *)
 
 open Pp
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6edc723cf..4e06fffb7 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 f81f15d89..1af19868a 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 1fdd4c16f..8c84b40d1 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