some notation for map_arrows2

[helm.git] / helm / software / matita / contribs / procedural / Coq / Coq.conf.xml

diff --git a/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml b/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml
index 8ef23325e5190ec048ff7f9b5fb4792a35e520c3..4c7d882b820db8fbebf01b5e910cf30c57d6963e 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml
+++ b/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml
@@ -5,10 +5,34 @@
     <key name="output_name">Coq</key>
     <key name="input_base_uri">cic:/Coq</key>
     <key name="output_base_uri">cic:/matita/procedural/Coq</key>
-    <key name="input_path">/projects/helm/exportation/V8.0_mowgli_bugfix_branch/theories</key>
+    <key name="input_path">/home/fguidi/coq_ufficial_theories/8.0pl2</key>
     <key name="output_path">contribs/procedural/Coq</key>
     <key name="input_type">.v</key>
     <key name="output_type">procedural</key>    
+
+    <key name="include">Arith/EqNat Init/Prelude</key>
+    <key name="include">Arith/Even Init/Prelude</key>
+    <key name="include">Arith/Le Init/Prelude</key>
+    <key name="include">Bool/Bool Init/Prelude</key>
+    <key name="include">Bool/DecBool Init/Prelude</key>
+    <key name="include">Bool/Sumbool Init/Prelude</key>
+    <key name="include">Lists/Streams Init/Prelude</key>
+    <key name="include">Logic/Berardi Init/Prelude</key>    
+    <key name="include">Logic/ChoiceFacts Init/Prelude</key>
+    <key name="include">Logic/ClassicalFacts Init/Prelude</key>
+    <key name="include">Logic/Decidable Init/Prelude</key>
+    <key name="include">Logic/Eqdep Init/Prelude</key>
+    <key name="include">Logic/Eqdep_dec Init/Prelude</key>
+    <key name="include">Logic/Hurkens Init/Prelude</key>
+    <key name="include">Logic/RelationalChoice Init/Prelude</key>
+    <key name="include">NArith/BinPos Init/Prelude</key>
+    <key name="include">Relations/Relation_Definitions Init/Prelude</key>
+    <key name="include">Relations/Rstar Init/Prelude</key>
+    <key name="include">Setoids/Setoid Init/Prelude</key>
+    <key name="include">Sets/Ensembles Init/Prelude</key>
+    <key name="include">Sets/Permut Init/Prelude</key>
+    <key name="include">Sets/Relations_1 Init/Prelude</key>
+    <key name="include">Wellfounded/Inverse_Image Init/Prelude</key>    
 <!--    
     <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con</key>
     <key name="coercion">Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2)</key>