aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-15 23:18:16 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-15 23:18:16 +0000
commit5c15d9a0ad129b0407cabfe202a142c91a34e110 (patch)
tree664cb6763ffd4841abb6b8098eba4eefe1c2edc2 /generic/proof.el
parentc9466a2b48c9e671600a5676a746fe463c94af9a (diff)
Comments.
Diffstat (limited to 'generic/proof.el')
-rw-r--r--generic/proof.el12
1 files changed, 7 insertions, 5 deletions
diff --git a/generic/proof.el b/generic/proof.el
index 3187f32c..7957177b 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -12,11 +12,13 @@
;; This file loads Proof General. It is required by the
;; individual prover modes. Loading order of PG is:
;;
-;; 1. proof-site (autoloads & stubs for mode functions)
-;; 2. autoload of <PA>/<PA>.el by auto-mode-alist
-;; 3. <PA>.el requires this file
-;; 4. rest of PG loaded here, inc proof-config/pg-custom
-;; 5. further modules loaded by autoloads.
+;; 1. proof-site (variables, autoloads & stubs for mode functions)
+;; 2. stub <PA>-mode function sets proof-assistant-symbol and related variables
+;; 3. prover-dependent variables defined in pg-custom
+;; 4. stub explicitly loads <PA>/<PA>.el and execute real mode function
+;; 5. <PA>.el requires this file, rest of PG loaded here
+;; 6. further modules loaded by autoloads/prover-specific requires.
+;;
;;
;;; Code: