From 5bc1672a263663a241ba8b0efde692b246761b6a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 31 Jul 2009 13:15:07 +0000 Subject: [PATCH] Bad patch reverted (in error message). --- helm/software/components/ng_refiner/nCicRefiner.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 0926db840..26fc593b7 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -510,8 +510,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he 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) - (List.length args_so_far)))) + (List.length args) (List.length args_so_far)))) | ty -> let metasenv, subst, newhead, newheadty = too_many_args := true; -- 2.39.2