Merge PR coq#6866: Slight improvement of messages related to direct a…

…nd indirect uses of tactic `clear`.

engine/evarutil.ml

@@ -534,7 +534,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
 
@@ -545,13 +545,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
@@ -599,8 +599,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

engine/evarutil.mli

@@ -232,7 +232,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

tactics/tactics.ml

@@ -198,32 +198,40 @@ end
 let convert x y = convert_gen Reduction.CONV x y
 let convert_leq x y = convert_gen Reduction.CUMUL x y
 
-let clear_dependency_msg env sigma id = function
+let clear_in_global_msg = function
+  | None -> mt ()
+  | Some ref -> str " implicitly in " ++ Printer.pr_global ref
+
+let clear_dependency_msg env sigma id err inglobal =
+  let pp = clear_in_global_msg inglobal in
+  match err with
   | Evarutil.OccurHypInSimpleClause None ->
-      Id.print id ++ str " is used in conclusion."
+      Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
   | Evarutil.OccurHypInSimpleClause (Some id') ->
-      Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"."
+      Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
   | Evarutil.EvarTypingBreak ev ->
       str "Cannot remove " ++ Id.print id ++
       strbrk " without breaking the typing of " ++
       Printer.pr_existential env sigma ev ++ str"."
 
-let error_clear_dependency env sigma id err =
-  user_err  (clear_dependency_msg env sigma id err)
+let error_clear_dependency env sigma id err inglobal =
+  user_err (clear_dependency_msg env sigma id err inglobal)
 
-let replacing_dependency_msg env sigma id = function
+let replacing_dependency_msg env sigma id err inglobal =
+  let pp = clear_in_global_msg inglobal in
+  match err with
   | Evarutil.OccurHypInSimpleClause None ->
-      str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion."
+      str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion."
   | Evarutil.OccurHypInSimpleClause (Some id') ->
       str "Cannot change " ++ Id.print id ++
-      strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"."
+      strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
   | Evarutil.EvarTypingBreak ev ->
       str "Cannot change " ++ Id.print id ++
       strbrk " without breaking the typing of " ++
       Printer.pr_existential env sigma ev ++ str"."
 
-let error_replacing_dependency env sigma id err =
-  user_err  (replacing_dependency_msg env sigma id err)
+let error_replacing_dependency env sigma id err inglobal =
+  user_err (replacing_dependency_msg env sigma id err inglobal)
 
 (* This tactic enables the user to remove hypotheses from the signature.
  * Some care is taken to prevent him from removing variables that are
@@ -242,7 +250,7 @@ let clear_gen fail = function
     let evdref = ref sigma in
     let (hyps, concl) =
       try clear_hyps_in_evi env evdref (named_context_val env) concl ids
-      with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+      with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
     in
     let env = reset_with_named_context hyps env in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
@@ -426,8 +434,8 @@ let clear_hyps2 env sigma ids sign t cl =
     let evdref = ref (Evd.clear_metas sigma) in
     let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
     (hyps, t, cl, !evdref)
-  with Evarutil.ClearDependencyError (id,err) ->
-    error_replacing_dependency env sigma id err
+  with Evarutil.ClearDependencyError (id,err,inglobal) ->
+    error_replacing_dependency env sigma id err inglobal
 
 let internal_cut_gen ?(check=true) dir replace id t =
   Proofview.Goal.enter begin fun gl ->
@@ -3007,8 +3015,24 @@ let unfold_body x =
   end
   end
 
+let warn_cannot_remove_as_expected =
+  CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics"
+         (fun (id,inglobal) ->
+           let pp = match inglobal with
+             | None -> mt ()
+             | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in
+           str "Cannot remove " ++ Id.print id ++ pp ++ str ".")
+
+let clear_for_destruct ids =
+  Proofview.tclORELSE
+    (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
+    (function
+     | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
+     | e -> iraise e)
+
 (* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
+let expand_hyp id =
+  Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id]
 
 (*****************************)
 (* High-level induction      *)