snapshot for CSC

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 26fc593b7dde5ab15ac86a6e6b401d2c84cc380b..48d1eeb1caa491631052740f68c3c159dada558c 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -378,7 +378,8 @@ and try_coercions rdb
       | NCicUnification.Uncertain _ as exc -> first exc tl
   in 
     first exc
-      (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty)
+      (NCicCoercion.look_for_coercion 
+        rdb metasenv subst context infty expty)
 
 and force_to_sort rdb metasenv subst context t orig_t localise ty =
   match NCicReduction.whd ~subst context ty with
@@ -440,27 +441,26 @@ and guess_name subst ctx ty =
 
 and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he he ty_he args =
   (*D*)inside 'E'; try let rc = 
-  let too_many_args = ref false in
   let rec aux metasenv subst args_so_far he ty_he = function 
   | [] ->
      let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
-      (match NCicReduction.whd ~subst context ty_he with
-          NCic.Meta _ | NCic.Appl (NCic.Meta _::_) ->
-           too_many_args := true;
-        | _ -> ());
       force_ty true false metasenv subst context orig_t res ty_he expty
   | NCic.Implicit `Vector::tl ->
+      let has_some_more_pis x =
+        match NCicReduction.whd ~subst context x with
+        |  NCic.Meta _ | NCic.Appl (NCic.Meta _::_) -> false
+        | _ -> true
+      in
      (try
-       too_many_args := false;
        aux metasenv subst args_so_far he ty_he tl
       with
-         Uncertain _
-       | RefineFailure _ as exc when !too_many_args <> true ->
-          try
+      | Uncertain _
+      | RefineFailure _ as exc when has_some_more_pis ty_he ->
+          (try
            aux metasenv subst args_so_far he ty_he
-            (NCic.Implicit `Vector :: NCic.Implicit `Term :: tl)
+            (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl)
           with
-           Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))
+           Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc)))
   | arg::tl ->
       match NCicReduction.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->
@@ -490,7 +490,6 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
           let metasenv, subst =
-             too_many_args := true;
              try NCicUnification.unify rdb metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
               ("The term %s has an inferred type %s, but is applied to the" ^^
@@ -506,14 +505,12 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
       | C.Match (_,_,C.Meta _,_) 
       | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
       | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
-          too_many_args := true;
           raise (Uncertain (lazy (localise orig_he, Printf.sprintf
             ("The term %s is here applied to %d arguments but expects " ^^
             "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
             (List.length args) (List.length args_so_far))))
       | ty ->
           let metasenv, subst, newhead, newheadty = 
-            too_many_args := true;
             try_coercions rdb ~localise metasenv subst context
               (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
               (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
@@ -523,7 +520,6 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
                "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
                (List.length args) (List.length args_so_far))))
           in
-           too_many_args := false;
            aux metasenv subst [] newhead newheadty (arg :: tl)
   in
    (* We need to reverse the order of the new created metas since they