[kernel] Property status: changes [automatically_proven] into [automatically_computed].

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} *)

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? *)
 
 (*

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 =