X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FCoq.conf.xml;h=4c7d882b820db8fbebf01b5e910cf30c57d6963e;hb=05cfeb82d2624860e66941421a937f308d66cf33;hp=8ef23325e5190ec048ff7f9b5fb4792a35e520c3;hpb=29714797b01e0ac8c22e4df2827b1785a759f482;p=helm.git
diff --git a/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml b/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml
index 8ef23325e..4c7d882b8 100644
--- a/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml
+++ b/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml
@@ -5,10 +5,34 @@
Coq
cic:/Coq
cic:/matita/procedural/Coq
- /projects/helm/exportation/V8.0_mowgli_bugfix_branch/theories
+ /home/fguidi/coq_ufficial_theories/8.0pl2
contribs/procedural/Coq
.v
procedural
+
+ Arith/EqNat Init/Prelude
+ Arith/Even Init/Prelude
+ Arith/Le Init/Prelude
+ Bool/Bool Init/Prelude
+ Bool/DecBool Init/Prelude
+ Bool/Sumbool Init/Prelude
+ Lists/Streams Init/Prelude
+ Logic/Berardi Init/Prelude
+ Logic/ChoiceFacts Init/Prelude
+ Logic/ClassicalFacts Init/Prelude
+ Logic/Decidable Init/Prelude
+ Logic/Eqdep Init/Prelude
+ Logic/Eqdep_dec Init/Prelude
+ Logic/Hurkens Init/Prelude
+ Logic/RelationalChoice Init/Prelude
+ NArith/BinPos Init/Prelude
+ Relations/Relation_Definitions Init/Prelude
+ Relations/Rstar Init/Prelude
+ Setoids/Setoid Init/Prelude
+ Sets/Ensembles Init/Prelude
+ Sets/Permut Init/Prelude
+ Sets/Relations_1 Init/Prelude
+ Wellfounded/Inverse_Image Init/Prelude