]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/engine.ml
- library/list/list.ma: unused code commented
[helm.git] / helm / software / components / binaries / transcript / engine.ml
index c55a1d19c70697c2528d487c6c05162e4c662d2a..39086d53fa86a4b7f3e89152be122f384366bbd4 100644 (file)
@@ -175,7 +175,7 @@ let is_ma st name =
 let set_items st name items =
    let i = get_index st name in
    let script = st.scripts.(i) in
-   let contents = List.rev_append items script.contents in
+   let contents = List.rev_append (X.list_uniq items) script.contents in
    st.scripts.(i) <- {script with name = name; contents = contents}
    
 let set_heading st name =