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 e54d5b48152098e8b33ffcec7a316a9a6d98a49a..b5d3d271dbd798880fa947b15b4652c660be9fed 100644 (file)
--- 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))