From 75b9cb11f623690c135dfe39b84065887f3f0f79 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 7 Dec 2006 18:19:57 +0000 Subject: [PATCH] avoid Failure "nth" when only one disambiguation pass is enabled --- helm/software/matita/dama/integration_algebras.ma | 2 +- helm/software/matita/matitaGui.ml | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma index 46bebc0e9..dc0ad9d32 100644 --- a/helm/software/matita/dama/integration_algebras.ma +++ b/helm/software/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/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index bd434ed74..79962a35c 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/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 -- 2.39.2