]> matita.cs.unibo.it Git - helm.git/commitdiff
Duplicated exception definition removed (used to give birth to a bug due to
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 7 Nov 2005 12:44:22 +0000 (12:44 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 7 Nov 2005 12:44:22 +0000 (12:44 +0000)
the generativeness of exceptions).

helm/ocaml/cic_disambiguation/disambiguateChoices.ml

index 99f8fca91634c9acb057c8d83beae1d247f6efeb..c660bb6b0a19895cd455ecdd08acf650097704b3 100644 (file)
@@ -27,7 +27,6 @@ open Printf
 
 open DisambiguateTypes
 
-exception Invalid_choice
 exception Choice_not_found of string Lazy.t
 
 let num_choices = ref []