diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-04 09:00:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-04 09:00:13 +0000 |
| commit | 9728a4b50d3c7da120cd384bb2eb3dcc02bd7585 (patch) | |
| tree | 7767f5d1a8f15a5ca4a0605217b7ad8897533e8e /proofs | |
| parent | d9ca83ef91f1092a4e5b35e329cc68da22e94027 (diff) | |
Confusion assert/error détectée par nouveau warning X de ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7508 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |