]> 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 c660bb6b0a19895cd455ecdd08acf650097704b3..b7f2410366dbf783059c0449ba2b068087d58862 100644 (file)
@@ -51,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)