From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 27 Jul 2005 07:54:03 +0000 (+0000)
Subject: bugfix: added xref on ast built via pattern matching from cic (3 -> 2)
X-Git-Tag: V_0_7_2~49
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e80eed78f048a235b44d2fd266c4b5a4dd951632;p=helm.git

bugfix: added xref on ast built via pattern matching from cic (3 -> 2)
---

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))