From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Sat, 13 Sep 2003 23:58:01 +0000 (+0000)
Subject: added environment file setting for each tutor
X-Git-Tag: V_0_4_3_4~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e723a887589e8fc163cfbe982b243e79a8855089;p=helm.git

added environment file setting for each tutor
---

diff --git a/helm/hbugs/tutors/INDEX.xml b/helm/hbugs/tutors/INDEX.xml
index 7936066b2..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
 
@@ -31,6 +32,7 @@
     <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>
 -->
 
@@ -41,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>
@@ -49,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>
@@ -57,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>
@@ -65,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>
@@ -73,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>
@@ -81,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>
@@ -89,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>
@@ -97,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>
@@ -105,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>
@@ -113,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>