...

[helm.git] / components / cic_disambiguation / disambiguateChoices.ml

diff --git a/components/cic_disambiguation/disambiguateChoices.ml b/components/cic_disambiguation/disambiguateChoices.ml
index bdbc9317908efe7dc29a9f3e11637a7761923ed0..c3fa7efb2805cf953cf9cee4545f69c416984ca5 100644 (file)
--- a/components/cic_disambiguation/disambiguateChoices.ml
+++ b/components/cic_disambiguation/disambiguateChoices.ml
@@ -47,16 +47,29 @@ let lookup_num_by_dsc dsc =
 let mk_choice (dsc, args, appl_pattern) =
   dsc,
   (fun env _ cic_args ->
-    let env' =
+    let env',rest =
       let names =
         List.map (function CicNotationPt.IdentArg (_, name) -> name) args
       in
-      try
-        List.combine names cic_args
-      with Invalid_argument _ ->
-       raise (Invalid_choice (lazy "The notation expects a different number of arguments"))
+       let rec combine_with_rest l1 l2 =
+        match l1,l2 with
+           _::_,[] -> raise (Invalid_argument "combine_with_rest")
+         | [],rest -> [],rest
+         | he1::tl1,he2::tl2 ->
+            let l,rest = combine_with_rest tl1 tl2 in
+             (he1,he2)::l,rest
+       in
+        try
+         combine_with_rest names cic_args
+        with Invalid_argument _ ->
+         raise (Invalid_choice (None, lazy ("The notation " ^ dsc ^ " expects more arguments")))
     in
-    TermAcicContent.instantiate_appl_pattern env' appl_pattern)
+     let combined =
+      TermAcicContent.instantiate_appl_pattern env' appl_pattern
+     in
+      match rest with
+         [] -> combined
+       | _::_ -> Cic.Appl (combined::rest))
 
 let lookup_symbol_by_dsc symbol dsc =
   try