X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=49bd256388480b11e04c48a4dd701d09ccbce29f;hb=0a167625079fa376ab027004453e8d042cde5b85;hp=c75e1aa3fa2ebe3549290262fb764349bc6244f2;hpb=c4c2dc8bc7fd9729ca43ff1ff484fca9ac7b963e;p=helm.git

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