X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=da07dd235489890fa39b5ec31d2aa3e47bcdb415;hb=7288b45eacf9f7dcd118b3b89b81ff19ae9d6ce5;hp=c55a1d19c70697c2528d487c6c05162e4c662d2a;hpb=14e2489ae86ecb6467fe9a7ba3b742a8d53c47ea;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index c55a1d19c..da07dd235 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -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 = 
@@ -201,9 +201,10 @@ let make_script_name st script name =
 let get_iparams st name =
    let debug debug = GA.IPDebug debug in
    let map = function
+      | "comments"   -> GA.IPComments
       | "nodefaults" -> GA.IPNoDefaults
       | "coercions"  -> GA.IPCoercions
-      | "comments"   -> GA.IPComments
+      | "cr"         -> GA.IPCR
       | s            -> 
 	 try Scanf.sscanf s "debug-%u" debug with
 	    | Scanf.Scan_failure _