X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2FINDEX.xml;h=bd4baad454b6dce9029fc53c2db73fa3540dca2d;hb=e723a887589e8fc163cfbe982b243e79a8855089;hp=7936066b28c399411778805dca8f616c2e12c9b0;hpb=d1010e05c0d73e3b44d3d971592bd8be9e1e0752;p=helm.git
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 @@
Hbugs_types.Use_ring_Luke
Use Ring Luke
WAIT FOREVER tutor
+ wait.environment
-->
@@ -41,6 +43,7 @@
Hbugs_types.Use_ring_Luke
Use Ring Luke
Ring tutor
+ ring.environment
127.0.0.1
@@ -49,6 +52,7 @@
Hbugs_types.Use_fourier_Luke
Use Fourier Luke
Fourier tutor
+ fourier.environment
127.0.0.1
@@ -57,6 +61,7 @@
Hbugs_types.Use_reflexivity_Luke
Use Reflexivity Luke
Reflexivity tutor
+ reflexivity.environment
127.0.0.1
@@ -65,6 +70,7 @@
Hbugs_types.Use_symmetry_Luke
Use Symmetry Luke
Symmetry tutor
+ symmetry.environment
127.0.0.1
@@ -73,6 +79,7 @@
Hbugs_types.Use_assumption_Luke
Use Assumption Luke
Assumption tutor
+ assumption.environment
127.0.0.1
@@ -81,6 +88,7 @@
Hbugs_types.Use_contradiction_Luke
Use Contradiction Luke
Contradiction tutor
+ contradiction.environment
127.0.0.1
@@ -89,6 +97,7 @@
Hbugs_types.Use_exists_Luke
Use Exists Luke
Exists tutor
+ exists.environment
127.0.0.1
@@ -97,6 +106,7 @@
Hbugs_types.Use_split_Luke
Use Split Luke
Split tutor
+ split.environment
127.0.0.1
@@ -105,6 +115,7 @@
Hbugs_types.Use_left_Luke
Use Left Luke
Left tutor
+ left.environment
127.0.0.1
@@ -113,15 +124,17 @@
Hbugs_types.Use_right_Luke
Use Right Luke
Right tutor
+ right.environment
-
+
127.0.0.1
50011
PrimitiveTactics.apply_tac
Hbugs_types.Use_apply_Luke
Use Apply Luke (with argument)
Search pattern apply tutor
+ search_pattern_apply.environment