to me, the problem:

[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 c4534e8daf6f466430f1144abf40ed28ed3c691a..7c199f8c07bf0c64ec295392f99083ad81b20db8 100644 (file)
--- 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