From: Stefano Zacchiroli <zack@upsilon.cc>
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