From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 10 Sep 2009 14:41:22 +0000 (+0000)
Subject: to me, the problem:
X-Git-Tag: make_still_working~3485
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=686f7f4f4444125885bc7ef9e8ec3e0b6f567137;p=helm.git

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 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
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 07eba73b5..c22470853 100644
--- 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 ->