]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/engine.ml
- some depend files fixed
[helm.git] / helm / software / components / binaries / transcript / engine.ml
index c55a1d19c70697c2528d487c6c05162e4c662d2a..da07dd235489890fa39b5ec31d2aa3e47bcdb415 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 = 
@@ -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 _