| [ 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)
in
aux []
-let dress sauce =
+let dress ~sep:sauce =
let rec aux =
function
| [] -> []
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
| 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