Commit 9cdaf336 authored by MARCHE Claude's avatar MARCHE Claude

cleaning detached: temporary work-around an unexpected assert failure

parent 01adab9a
......@@ -778,7 +778,9 @@ let proof_is_complete pa =
let clean c ~removed nid =
(* clean should not change proved status *)
let notification _ = assert false in
let notification any =
Format.eprintf "Cleaning error: cleaning attempts to change status of node %a@." fprintf_any any
in
let s = c.controller_session in
(* This function is applied on leafs first for the case of removes *)
let clean_aux () any =
......
......@@ -98,6 +98,14 @@ type any =
| APn of proofNodeID
| APa of proofAttemptID
let fprintf_any fmt a =
match a with
| AFile f -> Format.fprintf fmt "<AFile %s>" f.file_name
| ATh th -> Format.fprintf fmt "<ATh %s>" th.theory_name.Ident.id_string
| ATn trid -> Format.fprintf fmt "<ATn %d>" trid
| APn pnid -> Format.fprintf fmt "<APn %d>" pnid
| APa paid -> Format.fprintf fmt "<APa %d>" paid
module Hpn = Hint
module Htn = Hint
module Hpan = Hint
......
......@@ -45,6 +45,8 @@ type any =
| APn of proofNodeID
| APa of proofAttemptID
val fprintf_any: Format.formatter -> any -> unit
type notifier = any -> unit
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment