]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguateChoices.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_disambiguation / disambiguateChoices.ml
index 99f8fca91634c9acb057c8d83beae1d247f6efeb..b7f2410366dbf783059c0449ba2b068087d58862 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 []
@@ -52,7 +51,8 @@ let mk_choice (dsc, args, appl_pattern) =
       in
       try
         List.combine names cic_args
-      with Invalid_argument _ -> raise Invalid_choice
+      with Invalid_argument _ ->
+       raise (Invalid_choice (lazy "The notation expects a different number of arguments"))
     in
     CicNotationFwd.instantiate_appl_pattern env' appl_pattern)