From 4a612cd8684c60345c6f5a1f4f8fcc96fdc39685 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Sep 2006 21:35:36 +0000 Subject: [PATCH] Yet another refinement error localized. Enrico should really learn to localize his own exceptions :-) --- components/cic_unification/cicRefine.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 0ef14696c..c2c3902e4 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -1492,7 +1492,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst,metasenv,ugraph,hetype,he,args_bo_and_ty else (* this (says CSC) is also useful to infer dependent types *) - fix_arity metasenv context subst he hetype args_bo_and_ty ugraph + try + fix_arity metasenv context subst he hetype args_bo_and_ty ugraph + with RefineFailure _ | Uncertain _ as exn -> + (* unable to fix arity *) + more_args_than_expected localization_tbl + subst he context hetype args_bo_and_ty exn in let coerced_args,subst,metasenv,he,t,ugraph = eat_prods_and_args -- 2.39.2