X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=63f1eee58483af12e3dc946e2dd1d83da36ec930;hb=8a5c30a914d7ff665218b31853c6fb4bcf58aa08;hp=8ed903be16be436e09a4da2f61326fc562103040;hpb=d7aca3eacb4bd8dc56223098f92e5370c82f92ff;p=helm.git

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 8ed903be1..63f1eee58 100644
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -602,7 +602,7 @@ let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
      ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
-     ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
+     ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice ?create_dummy_ids:None)
      ~refine_thing:(refine_term status) (text,prefix_len,term)
      ~mk_localization_tbl ~expty ~subst
    in