From 0a167625079fa376ab027004453e8d042cde5b85 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 10 Jul 2009 03:16:06 +0000 Subject: [PATCH] Bug fixed (missing ctx) + comment added. --- helm/software/components/grafite_engine/grafiteEngine.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index c75e1aa3f..49bd25638 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -524,8 +524,9 @@ let eval_ncoercion status name t ty (id,src) tgt = else let metasenv,subst,status,src = GrafiteDisambiguate.disambiguate_nterm - None status [] [] [] ("",0,src) in + None status ctx [] [] ("",0,src) in let src = NCicUntrusted.apply_subst subst [] src in + (* HMM: ma tanto se ignori l'informazione, a che serve?? *) let _ = NCicUnification.unify status metasenv subst ctx ty src in src, cpos | _ -> assert false -- 2.39.2