bugfix: no more xref on bound names

[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index f2c2539cde31f20e5c4a8a7a2c6019b327e189fe..e4145e118984e5311195000ea52d9b5edd7720b9 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -336,7 +336,7 @@ let ungroup =
   in
     aux []
 
-let dress sauce =
+let dress ~sep:sauce =
   let rec aux =
     function
       | [] -> []
@@ -345,6 +345,15 @@ let dress sauce =
   in
     aux
 
+let dressn ~sep:sauces =
+  let rec aux =
+    function
+      | [] -> []
+      | [hd] -> [hd]
+      | hd :: tl -> hd :: sauces @ aux tl
+  in
+    aux
+
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function
@@ -370,9 +379,11 @@ let cic_name_of_name = function
   | CicNotationPt.Ident (name, None) -> Cic.Name name
   | _ -> assert false
 
-let name_of_cic_name = function
-  | Cic.Name s -> CicNotationPt.Ident (s, None)
-  | Cic.Anonymous -> CicNotationPt.Ident ("_", None)
+let name_of_cic_name =
+  let add_dummy_xref t = CicNotationPt.AttributedTerm (`IdRef "", t) in
+  function
+  | Cic.Name s -> add_dummy_xref (CicNotationPt.Ident (s, None))
+  | Cic.Anonymous -> add_dummy_xref (CicNotationPt.Ident ("_", None))
 
 let fresh_index = ref ~-1