From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Jul 2009 03:16:06 +0000 (+0000)
Subject: Bug fixed (missing ctx) + comment added.
X-Git-Tag: make_still_working~3705
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0a167625079fa376ab027004453e8d042cde5b85

Bug fixed (missing ctx) + comment added.
---

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