diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ca5d53587..fecddbefb 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -188,12 +188,8 @@ let lookup_tactic s = (* refiner r is a tactic applying the rule r *) -let bad_subproof () = - anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.") - let check_subproof_connection gl spfl = - if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl) - then (bad_subproof (); false) else true + list_for_all2eq (fun g pf -> g=pf.goal) gl spfl let abstract_tactic_expr te tacfun gls = let (sgl_sigma,v) = tacfun gls in |