diff options
| author | letouzey | 2013-03-13 00:00:12 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-13 00:00:12 +0000 |
| commit | 552df1605233769ad3cdabaadaa0011605e79797 (patch) | |
| tree | 28c3ae6a250aba80e1eb53ff9d906df9f49b75c1 /plugins/fourier | |
| parent | da3cbbcef1f4de9780603225e095f026bb5da709 (diff) | |
Restrict (try...with...) to avoid catching critical exn (part 7)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/fourier')
| -rw-r--r-- | plugins/fourier/fourier.ml | 23 | ||||
| -rw-r--r-- | plugins/fourier/fourierR.ml | 2 |
2 files changed, 12 insertions, 13 deletions
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index b940dee3a4..6266290632 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -164,20 +164,19 @@ qui donne 0 < c si s=true ou 0 <= c sinon cette inéquation étant absurde. *) + +exception Contradiction of (rational * bool * rational list) list + let unsolvable lie = let lr = deduce lie in - let res = ref [] in - (try (List.iter (fun e -> - match e with - {coef=[c];hist=lc;strict=s} -> - if (rinf c r0 && (not s)) || (rinfeq c r0 && s) - then (res := [c,s,lc]; - raise (Failure "contradiction found")) - |_->assert false) - lr) - with _ -> ()); - !res -;; + let check = function + | {coef=[c];hist=lc;strict=s} -> + if (rinf c r0 && (not s)) || (rinfeq c r0 && s) + then raise (Contradiction [c,s,lc]) + |_->assert false + in + try List.iter check lr; [] + with Contradiction l -> l (* Exemples: diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index fbb00285ce..0ec82425dc 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -40,7 +40,7 @@ type flin = {fhom: rational Constrhash.t; let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};; -let flin_coef f x = try (Constrhash.find f.fhom x) with _-> r0;; +let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;; let flin_add f x c = let cx = flin_coef f x in |