to me, the problem:

  ? t ==?== ?->?
where the first ? has an empty local context
is always Uncertain... to be fully understood
why unification gives Failure. It may be correct if
t has type (Rel k). I wrap it in the refiner.

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

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 07eba73b564385b6742ada4848bcb16be7f255fd..c224708533e5c6789606d943ac37fa4d23a609fb 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -95,6 +95,8 @@ let outside () =
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;
+let pp _ = ();;
+
 
 let ppcontext = NCicPp.ppcontext;;
 let ppmetasenv = NCicPp.ppmetasenv;;
@@ -102,8 +104,6 @@ let ppmetasenv = NCicPp.ppmetasenv;;
 let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "...";;
 let ppmetasenv ~subst:_subst _metasenv = "...";;
 
-let pp _ = ();;
-
 let fix_sorts swap exc t =
   let rec aux () = function
     | NCic.Sort (NCic.Type u) as orig ->