diff options
-rw-r--r-- | proofs/refiner.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 11f654c2e..fca4d85fe 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -144,7 +144,7 @@ let bad_subproof () = let check_subproof_connection gl spfl = if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl) - then bad_subproof () + then (bad_subproof (); false) else true let refiner = function | Prim pr as r -> @@ -153,7 +153,7 @@ let refiner = function let sgl = prim_fun (ts_it goal_sigma.sigma) goal_sigma.it in ({it=sgl; sigma = goal_sigma.sigma}, (fun spfl -> - if !Options.debug then check_subproof_connection sgl spfl; + assert (check_subproof_connection sgl spfl); { status = and_status (List.map pf_status spfl); goal = goal_sigma.it; subproof = None; @@ -166,7 +166,7 @@ let refiner = function let hidden_proof = v (List.map leaf sgl_sigma.it) in (sgl_sigma, fun spfl -> - if !Options.debug then check_subproof_connection sgl_sigma.it spfl; + assert (check_subproof_connection sgl_sigma.it spfl); { status = and_status (List.map pf_status spfl); goal = goal_sigma.it; subproof = Some hidden_proof; @@ -178,7 +178,7 @@ let refiner = function let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in ({it=[sg];sigma=goal_sigma.sigma}, (fun spfl -> - if !Options.debug then check_subproof_connection [sg] spfl; + assert (check_subproof_connection [sg] spfl); { status = (List.hd spfl).status; goal = gl; subproof = None; @@ -195,7 +195,7 @@ let refiner = function let sgl = [norm_goal (ts_it goal_sigma.sigma) sg] in ({it=sgl;sigma=goal_sigma.sigma}, (fun spfl -> - if !Options.debug then check_subproof_connection sgl spfl; + assert (check_subproof_connection sgl spfl); { status = (List.hd spfl).status; goal = gl; subproof = None; |