X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_notation%2FcicNotationUtil.ml;h=e4145e118984e5311195000ea52d9b5edd7720b9;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=4489344f53b58728d3b49fec4829350a05594b2b;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 4489344f5..e4145e118 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -319,6 +319,10 @@ let boxify = function
   | [ a ] -> a
   | l -> Layout (Box ((H, false, false), l))
 
+let unboxify = function
+  | Layout (Box ((H, false, false), [ a ])) -> a
+  | l -> l
+
 let group = function
   | [ a ] -> a
   | l -> Layout (Group l)
@@ -332,7 +336,7 @@ let ungroup =
   in
     aux []
 
-let dress sauce =
+let dress ~sep:sauce =
   let rec aux =
     function
       | [] -> []
@@ -341,6 +345,15 @@ let dress sauce =
   in
     aux
 
+let dressn ~sep:sauces =
+  let rec aux =
+    function
+      | [] -> []
+      | [hd] -> [hd]
+      | hd :: tl -> hd :: sauces @ aux tl
+  in
+    aux
+
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function
@@ -366,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