X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=7c199f8c07bf0c64ec295392f99083ad81b20db8;hb=b266ed97b63400d62ab4ba6a4ebdfbc1d5b0c2bb;hp=c4534e8daf6f466430f1144abf40ed28ed3c691a;hpb=c1f12859e933fdbd2ca5e054fc23c01f79f8cc56;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index c4534e8da..7c199f8c0 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -522,7 +522,11 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
               (NCicPp.ppterm ~metasenv ~subst ~context he)
               (NCicPp.ppterm ~metasenv ~subst ~context t)
               (NCicPp.ppterm ~metasenv ~subst ~context arg)
-              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
+              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) 
+                 (match exc with
+                 | NCicUnification.UnificationFailure m -> 
+                     NCicUnification.Uncertain m
+                 | x -> x))
               (* XXX coerce to funclass *)
           in
           let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in