From 2c5fc1a1783fc82d6a6b120b122a43a47f7cc5e0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Jul 2005 07:53:12 +0000 Subject: [PATCH] bugfix: no more xref on bound names --- helm/ocaml/cic_notation/cicNotationUtil.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) 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 -- 2.39.2