diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index e6eae23d70bc2188c05864ec06ac01ad72a44682..0bec8e3b4c0967268de037ef4ee358d67dde4d7c 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -694,27 +694,10 @@ and get_status ?(must_register=true) ppt =
 (* local alias: too much local definitions of get implies name clashes *)
 let get ppt = get_status ppt
 
-let automatically_proven ppt =
+let automatically_computed ppt =
   match property_kind ppt with
-  | Hypothesis | Unverifiable | Ignored | Other -> false
-  | Consequence _ | Tautology ->
-    (* nobody else tried to prove it *)
-    try
-      let by_emitter = Status.find ppt in
-      try
-        Emitter_with_properties.Hashtbl.iter
-          (fun e _ ->
-             if not (Emitter.equal
-                       (Emitter.Usable_emitter.get e.emitter)
-                       Emitter.kernel)
-             then raise Exit)
-          by_emitter;
-        true
-      with Exit ->
-        false
-    with Not_found ->
-      true
-
+  | Hypothesis | Unverifiable | Ignored | Consequence _ | Tautology -> true
+  | Other -> false
 
 (**************************************************************************)
 (** {3 Consolidated property status} *)
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index 3cf7daca5c6deb96e7e0df987ad8962e1e0e212f..5656c38152bc9d7009c892748ecdf561bed82fcf 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -261,8 +261,8 @@ val merge: old:Property.t list  -> Property.t list -> unit
 (** [merge old new] registers properties in [new] which are not in [old] and
     removes properties in [old] which are not in [new]. *)
 
-val automatically_proven: Property.t -> bool
-(** Is the status of the given property only automatically handled by the 
+val automatically_computed: Property.t -> bool
+(** Is the status of the given property only automatically handled by the
     kernel? *)
 
 (*
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index cffbd71e7888b40fd1a7d0f92d0dd589a45cddc6..f9c730b433d7558be89d8ba2b6c066f545400d2e 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -47,7 +47,7 @@ let code_annotation_loc ca stmt =
 
 let mark_unreachable () =
   let mark ppt =
-    if not (Property_status.automatically_proven ppt) then begin
+    if not (Property_status.automatically_computed ppt) then begin
       Value_parameters.debug "Marking property %a as dead"
         Description.pp_property ppt;
       let emit =