From e80eed78f048a235b44d2fd266c4b5a4dd951632 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Jul 2005 07:54:03 +0000 Subject: [PATCH] bugfix: added xref on ast built via pattern matching from cic (3 -> 2) --- helm/ocaml/cic_notation/cicNotationRew.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index e54d5b481..b5d3d271d 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -529,9 +529,10 @@ let rec ast_of_acic1 term_info annterm = with Not_found -> assert false in let ast = instantiate32 term_info env' symbol args in - match uris with - | [] -> ast - | _ -> Ast.AttributedTerm (`Href uris, ast) + Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), + (match uris with + | [] -> ast + | _ -> Ast.AttributedTerm (`Href uris, ast))) let load_patterns32 t = set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t)) -- 2.39.2