From: Stefano Zacchiroli Date: Thu, 7 Dec 2006 18:19:57 +0000 (+0000) Subject: avoid Failure "nth" when only one disambiguation pass is enabled X-Git-Tag: 0.4.95@7852~744 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7fed865c7cd7ea742a360158a931a3fa734ee446;p=helm.git avoid Failure "nth" when only one disambiguation pass is enabled --- diff --git a/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma index 46bebc0e9..dc0ad9d32 100644 --- a/matita/dama/integration_algebras.ma +++ b/matita/dama/integration_algebras.ma @@ -146,7 +146,7 @@ record integration_riesz_space (R:real) : Type \def ) * irs_unit))) 0; irs_quotient_space1: ∀f,g:irs_archimedean_riesz_space. - integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0 → f=g + integral (absolute_value irs_archimedean_riesz_space (f - g)) = 0 → f=g }. definition induced_norm_fun ≝ diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index bd434ed74..79962a35c 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -238,11 +238,13 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView. let remove_non_significant = List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in if all_passes then errorll else + let safe_list_nth l n = try List.nth l n with Failure _ -> [] in (* We remove passes 1,2 and 5,6 *) []::[] - ::(remove_non_significant (List.nth errorll 2)) - ::(remove_non_significant (List.nth errorll 3)) - ::[]::[] in + ::(remove_non_significant (safe_list_nth errorll 2)) + ::(remove_non_significant (safe_list_nth errorll 3)) + ::[]::[] + in let choices = let pass = ref 0 in List.flatten