Commit 7c1e9071 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

avoid detection failure in presence of unknown prover

parent 78f5354b
...@@ -309,7 +309,9 @@ let add_prover_shortcuts env prover = ...@@ -309,7 +309,9 @@ let add_prover_shortcuts env prover =
let add_id_prover_shortcut env id prover priority = let add_id_prover_shortcut env id prover priority =
match Hstr.find_opt env.prover_shortcuts id with match Hstr.find_opt env.prover_shortcuts id with
| Some (p,_) when p >= priority -> () | Some (p,_) when p >= priority -> ()
(*
| Some _ -> assert false | Some _ -> assert false
*)
| _ -> Hstr.replace env.prover_shortcuts id (priority,prover) | _ -> Hstr.replace env.prover_shortcuts id (priority,prover)
let prover_auto_levels = Hprover.create 5 let prover_auto_levels = Hprover.create 5
......
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