From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 27 Jul 2005 07:53:12 +0000 (+0000)
Subject: bugfix: no more xref on bound names
X-Git-Tag: V_0_7_2~51
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c5fc1a1783fc82d6a6b120b122a43a47f7cc5e0;p=helm.git

bugfix: no more xref on bound names
---

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 44b83fd1d..e4145e118 100644
--- 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