Use of standard OCaml syntax

[helm.git] / matita / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 59fe713e560d989766209f4d3a55b066bd92a335..63f1eee58483af12e3dc946e2dd1d83da36ec930 100644 (file)
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -103,7 +103,7 @@ let find_in_context name context =
   aux 1 context
 
 let interpretate_term_and_interpretate_term_option (status: #NCic.status)
-  ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
+  ~create_dummy_ids ~obj_context ~mk_choice ~env ~uri ~is_path
   ~localization_tbl 
 =
   (* create_dummy_ids shouldbe used only for interpretating patterns *)
@@ -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