X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2FINDEX.xml;h=bd4baad454b6dce9029fc53c2db73fa3540dca2d;hb=faf362d25c28585add8c951300da0a54993d0d67;hp=9de3517095206c2fcfa0c598d1e8ea42f4f794af;hpb=ed90e027472d0250d45ae7200600c8804dd476f1;p=helm.git

diff --git a/helm/hbugs/tutors/INDEX.xml b/helm/hbugs/tutors/INDEX.xml
index 9de351709..bd4baad45 100644
--- a/helm/hbugs/tutors/INDEX.xml
+++ b/helm/hbugs/tutors/INDEX.xml
@@ -11,6 +11,7 @@
   @HINT_TYPE@         hint type (3rd argument of Hbugs_types.Register_tutor type
                       constructor, must have type Hbugs_types.hint_type)
   @DESCRIPTION@       human readable tutor description
+  @ENVIRONMENT_FILE@  file from which restore proof checking environment on boot
 
   "source" attribute  corresponding OCaml source file
 
@@ -21,6 +22,20 @@
 -->
 
 <tutors>
+
+  <!-- DEBUGGING -->
+<!--
+  <tutor source="wait_tutor.ml">
+    <addr>127.0.0.1</addr>
+    <port>50111</port>
+    <tactic>Wait.wait_tac</tactic>
+    <hint>Hbugs_types.Use_ring_Luke</hint>
+    <hint_type>Use Ring Luke</hint_type>
+    <description>WAIT FOREVER tutor</description>
+    <environment_file>wait.environment</environment_file>
+  </tutor>
+-->
+
   <tutor source="ring_tutor.ml">
     <addr>127.0.0.1</addr>
     <port>50001</port>
@@ -28,6 +43,7 @@
     <hint>Hbugs_types.Use_ring_Luke</hint>
     <hint_type>Use Ring Luke</hint_type>
     <description>Ring tutor</description>
+    <environment_file>ring.environment</environment_file>
   </tutor>
   <tutor source="fourier_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -36,6 +52,7 @@
     <hint>Hbugs_types.Use_fourier_Luke</hint>
     <hint_type>Use Fourier Luke</hint_type>
     <description>Fourier tutor</description>
+    <environment_file>fourier.environment</environment_file>
   </tutor>
   <tutor source="reflexivity_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -44,6 +61,7 @@
     <hint>Hbugs_types.Use_reflexivity_Luke</hint>
     <hint_type>Use Reflexivity Luke</hint_type>
     <description>Reflexivity tutor</description>
+    <environment_file>reflexivity.environment</environment_file>
   </tutor>
   <tutor source="symmetry_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -52,6 +70,7 @@
     <hint>Hbugs_types.Use_symmetry_Luke</hint>
     <hint_type>Use Symmetry Luke</hint_type>
     <description>Symmetry tutor</description>
+    <environment_file>symmetry.environment</environment_file>
   </tutor>
   <tutor source="assumption_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -60,6 +79,7 @@
     <hint>Hbugs_types.Use_assumption_Luke</hint>
     <hint_type>Use Assumption Luke</hint_type>
     <description>Assumption tutor</description>
+    <environment_file>assumption.environment</environment_file>
   </tutor>
   <tutor source="contradiction_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -68,6 +88,7 @@
     <hint>Hbugs_types.Use_contradiction_Luke</hint>
     <hint_type>Use Contradiction Luke</hint_type>
     <description>Contradiction tutor</description>
+    <environment_file>contradiction.environment</environment_file>
   </tutor>
   <tutor source="exists_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -76,6 +97,7 @@
     <hint>Hbugs_types.Use_exists_Luke</hint>
     <hint_type>Use Exists Luke</hint_type>
     <description>Exists tutor</description>
+    <environment_file>exists.environment</environment_file>
   </tutor>
   <tutor source="split_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -84,6 +106,7 @@
     <hint>Hbugs_types.Use_split_Luke</hint>
     <hint_type>Use Split Luke</hint_type>
     <description>Split tutor</description>
+    <environment_file>split.environment</environment_file>
   </tutor>
   <tutor source="left_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -92,6 +115,7 @@
     <hint>Hbugs_types.Use_left_Luke</hint>
     <hint_type>Use Left Luke</hint_type>
     <description>Left tutor</description>
+    <environment_file>left.environment</environment_file>
   </tutor>
   <tutor source="right_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -100,15 +124,17 @@
     <hint>Hbugs_types.Use_right_Luke</hint>
     <hint_type>Use Right Luke</hint_type>
     <description>Right tutor</description>
+    <environment_file>right.environment</environment_file>
   </tutor>
   <tutor source="search_pattern_apply_tutor.ml">
-    <no_auto />
+    <no_auto /> <!-- this imply that settings below are not significant -->
     <addr>127.0.0.1</addr>
     <port>50011</port>
     <tactic>PrimitiveTactics.apply_tac</tactic>
     <hint>Hbugs_types.Use_apply_Luke</hint>
     <hint_type>Use Apply Luke (with argument)</hint_type>
     <description>Search pattern apply tutor</description>
+    <environment_file>search_pattern_apply.environment</environment_file>
   </tutor>
 </tutors>