Improving error message for clear tactic (and indirect uses of it).

- Be more precise when trying to clear an hypothesis which
  occurs implicitly in a global constant.
- Warns if destruct/induction cannot clear an hypothesis occurring
  implicitly in a global.

In the first case, the change in situation

  Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a.

is:

- before: "a is used in conclusion"
- after: "a is used implicitly in b in conclusion"

In the second case:

  Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a.

produces a warning: "Cannot remove a, it is used implicitly in b".

2 files changed, 6 insertions, 6 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 065b42bf6..10ece69fa 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -522,7 +522,7 @@ type clear_dependency_error =
 | OccurHypInSimpleClause of Id.t option
 | EvarTypingBreak of existential
 
-exception ClearDependencyError of Id.t * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option
 
 exception Depends of Id.t
 
@@ -533,13 +533,13 @@ let rec check_and_clear_in_constr env evdref err ids global c =
      is a section variable *)
     match kind c with
       | Var id' ->
-      if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
+      if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c
 
       | ( Const _ | Ind _ | Construct _ ) ->
         let () = if global then
           let check id' =
             if Id.Set.mem id' ids then
-              raise (ClearDependencyError (id',err))
+              raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
           in
           Id.Set.iter check (Environ.vars_of_global env c)
         in
@@ -587,8 +587,8 @@ let rec check_and_clear_in_constr env evdref err ids global c =
                 let global = Id.Set.exists is_section_variable nids in
                 let concl = EConstr.Unsafe.to_constr (evar_concl evi) in
                 check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl
-	      with ClearDependencyError (rid,err) ->
-		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
+              with ClearDependencyError (rid,err,where) ->
+                raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in
 
             if Id.Map.is_empty rids then c
             else
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 40c1ee082..831a7f26b 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -224,7 +224,7 @@ type clear_dependency_error =
 | OccurHypInSimpleClause of Id.t option
 | EvarTypingBreak of Constr.existential
 
-exception ClearDependencyError of Id.t * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option
 
 val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types