From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Nov 2005 12:44:22 +0000 (+0000)
Subject: Duplicated exception definition removed (used to give birth to a bug due to
X-Git-Tag: V_0_7_2_3~117
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f2724b64f78339cc7b652e9514813c1705605b0;p=helm.git

Duplicated exception definition removed (used to give birth to a bug due to
the generativeness of exceptions).
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
index 99f8fca91..c660bb6b0 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
@@ -27,7 +27,6 @@ open Printf
 
 open DisambiguateTypes
 
-exception Invalid_choice
 exception Choice_not_found of string Lazy.t
 
 let num_choices = ref []