helm/software/matita/contribs/procedural/Coq/Coq.conf.xml

   1 <?xml version="1.0" encoding="utf-8"?>
   2 <helm_registry>
   3   <section name="package">
   4     <key name="input_name">Coq</key>
   5     <key name="output_name">Coq</key>
   6     <key name="input_base_uri">cic:/Coq</key>
   7     <key name="output_base_uri">cic:/matita/procedural/Coq</key>
   8     <key name="input_path">/home/fguidi/coq_ufficial_theories/8.0pl2</key>
   9     <key name="output_path">contribs/procedural/Coq</key>
  10     <key name="input_type">.v</key>
  11     <key name="output_type">procedural</key>
  12
  13     <key name="include">Arith/EqNat Init/Prelude</key>
  14     <key name="include">Arith/Even Init/Prelude</key>
  15     <key name="include">Arith/Le Init/Prelude</key>
  16     <key name="include">Bool/Bool Init/Prelude</key>
  17     <key name="include">Bool/DecBool Init/Prelude</key>
  18     <key name="include">Bool/Sumbool Init/Prelude</key>
  19     <key name="include">Lists/Streams Init/Prelude</key>
  20     <key name="include">Logic/Berardi Init/Prelude</key>
  21     <key name="include">Logic/ChoiceFacts Init/Prelude</key>
  22     <key name="include">Logic/ClassicalFacts Init/Prelude</key>
  23     <key name="include">Logic/Decidable Init/Prelude</key>
  24     <key name="include">Logic/Eqdep Init/Prelude</key>
  25     <key name="include">Logic/Eqdep_dec Init/Prelude</key>
  26     <key name="include">Logic/Hurkens Init/Prelude</key>
  27     <key name="include">Logic/RelationalChoice Init/Prelude</key>
  28     <key name="include">NArith/BinPos Init/Prelude</key>
  29     <key name="include">Relations/Relation_Definitions Init/Prelude</key>
  30     <key name="include">Relations/Rstar Init/Prelude</key>
  31     <key name="include">Setoids/Setoid Init/Prelude</key>
  32     <key name="include">Sets/Ensembles Init/Prelude</key>
  33     <key name="include">Sets/Permut Init/Prelude</key>
  34     <key name="include">Sets/Relations_1 Init/Prelude</key>
  35     <key name="include">Wellfounded/Inverse_Image Init/Prelude</key>
  36 <!--
  37     <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con</key>
  38     <key name="coercion">Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2)</key>
  39     <key name="coercion">nat_of_P cic:/Coq/NArith/BinPos/nat_of_P.con</key>
  40 -->
  41   </section>
  42 </helm_registry>