From 686f7f4f4444125885bc7ef9e8ec3e0b6f567137 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2009 14:41:22 +0000 Subject: [PATCH] =?utf8?q?to=20me,=20the=20problem:=20=20=20=3F=20t=20=3D?= =?utf8?q?=3D=3F=3D=3D=20=3F->=3F=20where=20the=20first=20=3F=20has=20an?= =?utf8?q?=20empty=20local=20context=20is=20always=20Uncertain...=20to=20b?= =?utf8?q?e=20fully=20understood=20why=20unification=20gives=20Failure.=20?= =?utf8?q?It=20may=20be=20correct=20if=20t=20has=20type=20(Rel=20k).=20I?= =?utf8?q?=20wrap=20it=20in=20the=20refiner.?= --- helm/software/components/ng_refiner/nCicRefiner.ml | 6 +++++- helm/software/components/ng_refiner/nCicUnification.ml | 4 ++-- 2 files changed, 7 insertions(+), 3 deletions(-) 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 -> -- 2.39.2