From: Stefano Zacchiroli 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 @@ 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