Better handling of idref propagation, no more Href hack, multiple idrefs are

[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 426846877617a054fade73112c31944aaf03673f..966e0262626b2e6a636ea374c50ed487bb13edea 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -160,6 +160,12 @@ let rec strip_attributes t =
   in
   visit_ast ~special_k strip_attributes t
 
+let rec get_idrefs =
+  function
+  | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t
+  | Ast.AttributedTerm (_, t) -> get_idrefs t
+  | _ -> []
+
 let meta_names_of_term term =
   let rec names = ref [] in
   let add_name n =
@@ -297,7 +303,7 @@ let dressn ~sep:sauces =
   in
     aux
 
-let find_appl_pattern_uris ap =
+(* let find_appl_pattern_uris ap =
   let rec aux acc =
     function
     | Ast.UriPattern uri ->
@@ -309,7 +315,7 @@ let find_appl_pattern_uris ap =
     | Ast.VarPattern _ -> acc
     | Ast.ApplPattern apl -> List.fold_left aux acc apl
   in
-  aux [] ap
+  aux [] ap *)
 
 let rec find_branch =
   function