]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
Huge reorganization of matita and ocaml.
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index 2ab3b37060cd66829a9696e4206b099a20687ae3..68946097381d574a4d37537a078e4ab443550ba4 100644 (file)
@@ -409,7 +409,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in
-   aux ~localize:true dummy_floc context ast
+   aux ~localize:true HExtlib.dummy_floc context ast
 
 let interpretate_path ~context path =
  let localization_tbl = Cic.CicHash.create 23 in
@@ -536,7 +536,7 @@ let rev_uniq =
 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
  * Domain item more in deep in the list will be processed first.
  *)
-let rec domain_rev_of_term ?(loc = dummy_floc) context = function
+let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
   | CicNotationPt.AttributedTerm (`Loc loc, term) ->
      domain_rev_of_term ~loc context term
   | CicNotationPt.AttributedTerm (_, term) ->