]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_disambiguation/nCicDisambiguate.ml
Porting to ocaml 5
[helm.git] / matita / components / ng_disambiguation / nCicDisambiguate.ml
index 59fe713e560d989766209f4d3a55b066bd92a335..8ed903be16be436e09a4da2f61326fc562103040 100644 (file)
@@ -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 *)