Fixed bug in notation: when a notation is applied to more arguments than expected...

diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml
index bdbc9317908efe7dc29a9f3e11637a7761923ed0..64d2cf8e0343155736784a6c67d9370fc9ab8343 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/software/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 (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