X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=39d4d8dddb20dac25dd7437c6595a8987036882a;hb=560db5569f54fba5bded568699a33947f88df3ba;hp=da07dd235489890fa39b5ec31d2aa3e47bcdb415;hpb=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git

diff --git a/matita/components/binaries/transcript/engine.ml b/matita/components/binaries/transcript/engine.ml
index da07dd235..39d4d8ddd 100644
--- a/matita/components/binaries/transcript/engine.ml
+++ b/matita/components/binaries/transcript/engine.ml
@@ -198,22 +198,6 @@ let make_script_name st script name =
    let ext = if script.is_ma then ".ma" else ".mma" in
    Filename.concat st.output_path (name ^ ext)
 
-let get_iparams st name =
-   let debug debug = GA.IPDebug debug in
-   let map = function
-      | "comments"   -> GA.IPComments
-      | "nodefaults" -> GA.IPNoDefaults
-      | "coercions"  -> GA.IPCoercions
-      | "cr"         -> GA.IPCR
-      | s            -> 
-	 try Scanf.sscanf s "debug-%u" debug with
-	    | Scanf.Scan_failure _
-	    | Failure _
-	    | End_of_file ->
-	       failwith ("unknown inline parameter: " ^ s)
-   in
-   List.map map (X.list_assoc_all name st.iparams) 
-
 let commit st name =
    let i = get_index st name in
    let script = st.scripts.(i) in
@@ -241,20 +225,14 @@ let produce st =
       let in_base_uri = Filename.concat st.input_base_uri name in
       let out_base_uri = Filename.concat st.output_base_uri name in
       let filter path = function
-         | T.Inline (b, k, obj, p, f, params)   -> 
+         | T.Inline (b, k, obj, p, f)   -> 
 	    let obj, p = 
 	       if b then Filename.concat (make_path path) obj, make_prefix path
 	       else obj, p
 	    in
 	    let ext = G.string_of_inline_kind k in
 	    let s = Filename.concat in_base_uri (obj ^ ext) in
-	    let params = 
-	       params @
-	       get_iparams st "*" @
-	       get_iparams st ("*" ^ ext) @
-	       get_iparams st (Filename.concat name obj)
-	    in
-	    path, Some (T.Inline (b, k, s, p, f, params))
+	    path, Some (T.Inline (b, k, s, p, f))
 	 | T.Include (moo, s)           ->
 	    begin 
 	       try path, Some (T.Include (moo, List.assoc s st.requires))