Bug fixed (missing ctx) + comment added.

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index c75e1aa3fa2ebe3549290262fb764349bc6244f2..49bd256388480b11e04c48a4dd701d09ccbce29f 100644 (file)
--- 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