update in lambdadelta

[helm.git] / matita / components / binaries / probe / options.ml

diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml
index ce29c1ef0f7499b6e9e16b8b4275865c3a4f6fd0..0b9487d6bf68d6d15ed8f4faba317b4ae76fa54c 100644 (file)
--- a/matita/components/binaries/probe/options.ml
+++ b/matita/components/binaries/probe/options.ml
@@ -1,12 +1,12 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 module A = Array
@@ -44,6 +44,8 @@ let default_objs = US.empty
 
 let default_srcs = US.empty
 
+let default_names = US.empty
+
 let default_remove = []
 
 let default_exclude = []
@@ -66,6 +68,8 @@ let objs = ref default_objs
 
 let srcs = ref default_srcs
 
+let names = ref default_names
+
 let remove = ref default_remove
 
 let exclude = ref default_exclude
@@ -113,8 +117,8 @@ let out_deps file =
 
 let clear () =
   R.clear (); A.iteri clear_slot slot;
-  objs := default_objs; srcs := default_srcs; remove := default_remove;
-  exclude := default_exclude; net := default_net;
+  objs := default_objs; srcs := default_srcs; names := default_names;
+  remove := default_remove; exclude := default_exclude; net := default_net;
   chars := default_chars; debug_lexer := default_debug_lexer;
   no_devel := default_no_devel; no_init := default_no_init;
   deps := UPS.empty