From 9728a4b50d3c7da120cd384bb2eb3dcc02bd7585 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 4 Nov 2005 09:00:13 +0000
Subject: 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
---
 proofs/refiner.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ca5d53587d..fecddbefb7 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
-- 
cgit v1.2.3