Stricter type: the type now shows that disambiguation only alter the lexicon.

[helm.git] / helm / software / matita / matitaEngine.ml

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 6e6213734d583422c5732471376ea3e0ff640869..6b16891c883621460ccfb5c7133eebd4aa465067 100644 (file)
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -61,7 +61,7 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context =
 let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) =
  let lexicon_status = GrafiteTypes.get_estatus grafite_status in
  let dump = not (Helm_registry.get_bool "matita.moo") in
- let lexicon_status_ref = ref lexicon_status in
+ let lexicon_status_ref = ref (lexicon_status :> LexiconEngine.status) in
  let baseuri = GrafiteTypes.get_baseuri grafite_status in
  let new_grafite_status,new_objs =
   match ast with