]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_disambiguation/nCicDisambiguate.ml
Use of standard OCaml syntax
[helm.git] / matita / components / ng_disambiguation / nCicDisambiguate.ml
index 8ed903be16be436e09a4da2f61326fc562103040..63f1eee58483af12e3dc946e2dd1d83da36ec930 100644 (file)
@@ -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