..

[helm.git] / matita / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index f82759195dae6bf5e50fbba9add0ed7fe09c09bc..7511e02aaad65670504ea7a23cd0902990da0148 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -28,16 +28,14 @@
 class type g_status =
   object
    inherit LexiconTypes.g_status
-   inherit NCicCoercion.g_status
   end
 
 class status =
  object (self)
   inherit LexiconTypes.status
-  inherit NCicCoercion.status
   method set_grafite_disambiguate_status
    : 'status. #g_status as 'status -> 'self
-      = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o
+      = fun o -> (self#set_lexicon_engine_status o)
  end
 
 exception BaseUriNotSetYet
@@ -138,7 +136,8 @@ let disambiguate_nterm expty estatus context metasenv subst thing
         ~context ~metasenv ~subst thing)
   in
   let estatus =
-    LexiconEngine.set_proof_aliases estatus GrafiteAst.WithPreferences diff
+    LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
+     GrafiteAst.WithPreferences diff
   in
    metasenv, subst, estatus, cic
 ;;
@@ -219,7 +218,9 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~aliases:estatus#lstatus.LexiconTypes.aliases
       ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases) 
       (text,prefix_len,obj)) in
-  let estatus = LexiconEngine.set_proof_aliases estatus
-  GrafiteAst.WithPreferences diff in
+  let estatus =
+   LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
+    GrafiteAst.WithPreferences diff
+  in
    estatus, cic
 ;;