bugfix: no more xref on bound names

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 44b83fd1d6609e87bbc3df836f37d00d9a14c0e4..e4145e118984e5311195000ea52d9b5edd7720b9 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -379,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