Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

author: Samuel Mimram <smimram@debian.org> 2008-07-25 15:12:53 +0200
committer: Samuel Mimram <smimram@debian.org> 2008-07-25 15:12:53 +0200
commit: a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
tree: dabcac548e299fee1da464c93b3dba98484f45b1 /dev
parent: 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
18 files changed, 3122 insertions, 2591 deletions
diff --git a/dev/base_include b/dev/base_include
index b7fa38ea..398f60d2 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -19,6 +19,7 @@
 
 #install_printer  (* identifier *) ppid;;
 #install_printer  (* identifier *) ppidset;;
+#install_printer  (* Intset.t *) ppintset;;
 #install_printer  (* label *) pplab;;
 #install_printer  (* mod_self_id *) ppmsid;;
 #install_printer  (* mod_bound_id *) ppmbid;;
@@ -31,6 +32,9 @@
 #install_printer  (* constr *)  print_pure_constr;; 
 #install_printer  (* patch *) ppripos;;
 #install_printer  (* values *) ppvalues;;
+#install_printer  (* Idpred.t *) pp_idpred;;
+#install_printer  (* Cpred.t *) pp_cpred;;
+#install_printer  (* transparent_state *) pp_transparent_state;;
 #install_printer ppzipper;;
 #install_printer ppstack;;
 #install_printer ppatom;;
@@ -38,6 +42,7 @@
 #install_printer ppvblock;;
 #install_printer  (* bigint *) ppbigint;;
 #install_printer  (* loc *) pploc;;
+#install_printer  (* substitution *) prsubst;;
 
 (* Open main files *)
 
@@ -63,12 +68,14 @@ open Pattern
 open Cbv
 open Classops
 open Pretyping
+open Pretyping.Default
+open Pretyping.Default.Cases
 open Cbv
 open Classops
-open Pretyping
 open Clenv
 open Rawterm
 open Coercion
+open Coercion.Default
 open Recordops
 open Detyping
 open Reductionops
@@ -82,6 +89,7 @@ open Indrec
 open Typing
 open Inductiveops
 open Unification
+open Matching
 
 open Constrextern
 open Constrintern
@@ -167,7 +175,7 @@ open Declarations;;
 
 let constbody_of_string s =
   let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in
-  Util.out_some b.const_body;;
+  Option.get b.const_body;;
 
 (* Get the current goal *)
 
diff --git a/dev/db b/dev/db
index 784e5bac..6221462a 100644
--- a/dev/db
+++ b/dev/db
@@ -3,6 +3,7 @@ load_printer "printers.cma"
 
 install_printer Top_printers.ppid
 install_printer Top_printers.ppidset
+install_printer Top_printers.ppintset
 install_printer Top_printers.pplab
 install_printer Top_printers.ppmsid
 install_printer Top_printers.ppmbid
@@ -20,6 +21,7 @@ install_printer Top_printers.pprawconstr
 install_printer Top_printers.ppconstr
 install_printer Top_printers.ppuni
 install_printer Top_printers.ppuniverses
+install_printer Top_printers.ppconstraints
 install_printer Top_printers.pptype
 install_printer Top_printers.ppj
 install_printer Top_printers.ppenv
@@ -27,6 +29,7 @@ install_printer Top_printers.ppenv
 install_printer Top_printers.ppgoal
 install_printer Top_printers.ppsigmagoal
 install_printer Top_printers.pproof
+install_printer Top_printers.ppmetas
 install_printer Top_printers.ppevd
 install_printer Top_printers.ppevm
 install_printer Top_printers.ppclenv
@@ -34,5 +37,6 @@ install_printer Top_printers.ppclenv
 install_printer Top_printers.pptac
 install_printer Top_printers.ppobj
 install_printer Top_printers.pploc
+install_printer Top_printers.prsubst
                                                   
 
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
new file mode 100644
index 00000000..c825f088
--- /dev/null
+++ b/dev/doc/build-system.dev.txt
@@ -0,0 +1,70 @@
+Since July 2007, Coq features a build system overhauled by Pierre
+Corbineau and Lionel Elie Mamane.
+
+This file documents internals of the implementation of the build
+system. For what a Coq developer needs to know about the build system,
+see build-system.txt .
+
+.ml4 files
+----------
+
+.ml files corresponding to .ml4 files are created to keep ocamldep
+happy only. To ensure they are not used for compilation, they contain
+invalid OCaml.
+
+multi-stage build
+-----------------
+
+Le processus de construction est séparé en trois étapes qui correspondent
+aux outils nécessaires pour calculer les dépendances de cette étape:
+
+stage1: ocamldep, sed , camlp4 sans fichiers de Coq
+stage2: camlp4 avec grammar.cma et/ou q_constr.cmo
+stage3: coqdep (.vo)
+
+Le Makefile a été séparé en plusieurs fichiers :
+
+- Makefile: coquille vide qui délègue les cibles à la bonne étape sauf
+  clean et les fichiers pour emacs (car ils sont en quelque sorte en
+  "stage0": aucun calcul de dépendance nécessaire).
+- Makefile.common : définitions des variables (essentiellement des
+  listes de fichiers)
+- Makefile.build : les règles de compilation sans inclure de
+  dépendances
+- Makefile.stage* : fichiers qui incluent les dépendances calculables
+  à cette étape ainsi que Makefile.build.
+
+The build needs to be cut in stages because make will not take into
+account one include when making another include.
+
+Parallélisation
+---------------
+
+Le découpage en étapes veut dire que le makefile est un petit peu
+moins parallélisable que strictement possible en théorie: par exemple,
+certaines choses faites en stage2 pourraient être faites en parallèle
+avec des choses de stage1. Nous essayons de minimiser cet effet, mais
+nous ne l'avons pas complètement éliminé parce que cela mènerait à un
+makefile très complexe. La minimisation est principalement que si on
+demande un objet spécifique (par exemple "make parsing/g_constr.cmx"),
+il est fait dans l'étape la plus basse possible (simplement), mais si
+un objet est fait comme dépendance de la cible demandée (par exemple
+dans un "make world"), il est fait le plus tard possible (par exemple,
+tout code OCaml non nécessaire pour coqdep ni grammar.cma ni
+q_constr.cmo est compilé en stage3 lors d'un "make world"; cela permet
+le parallélisme de compilation de code OCaml et de fichiers Coq (.v)).
+
+Le "(simplement)" ci-dessus veut dire que savoir si un fichier non
+nécessaire pour grammar.cma/q_constr.cmo peut en fait être fait en
+stage1 est compliqué avec make, alors nous retombons en général sur le
+stage2. La séparation entre le stage2 et stage3 est plus facile, donc
+l'optimisation ci-dessus s'y applique pleinement.
+
+En d'autres mots, nous avons au niveau conceptuel deux assignations
+d'étape pour chaque fichier:
+
+ - l'étape la plus petite où nous savons qu'il peut être fait.
+ - l'étape la plus grande où il peut être fait.
+
+Mais seule la première est gérée explicitement, la seconde est
+implicite.
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
new file mode 100644
index 00000000..c9571f7c
--- /dev/null
+++ b/dev/doc/build-system.txt
@@ -0,0 +1,299 @@
+Since July 2007, Coq features a build system overhauled by Pierre
+Corbineau and Lionel Elie Mamane.
+
+This file documents what a Coq developer needs to know about the build
+system. If you want to enhance the build system itself (or are curious
+about its implementation details), see build-system.dev.txt .
+
+The build system is not at its optimal state, see TODO section.
+
+Stages in build system
+----------------------
+
+The build system is separated into three stages, corresponding to the
+tool(s) necessary to compute the dependencies necessary at this stage:
+
+stage1: ocamldep, sed, camlp4 without Coq extensions
+stage2: camlp4 with grammar.cma and/or q_constr.cmo
+stage3: coqdep (.vo)
+
+The file "Makefile" itself serves as minimum stage for targets that
+should not need any dependency (such as *clean*).
+
+Changes (for old-timers)
+------------------------
+
+The contents of the old Makefile has been mostly split into:
+
+ - variable declarations for file lists in Makefile.common.
+
+   These declarations are now static (for faster Makefile execution),
+   so their definitions are order-dependent.
+
+ - actual building rules and compiler flags variables in
+   Makefile.build
+
+
+The handling of globals is now: the globals of FOO.v are in FOO.glob
+and the global glob.dump is created by concatenation of all .glob
+files. In particular, .glob files are now always created.
+
+See also section "cleaning targets"
+
+Reducing build system overhead
+------------------------------
+
+When you are actively working on a file in a "make a change, make to
+test, make a change, make to test", etc mode, here are a few tips to
+save precious time:
+
+ - Always ask for what you want directly (e.g. bin/coqtop,
+   foo/bar.cmo, ...), don't do "make world" and interrupt
+   it when it has done what you want. This will try to minimise the
+   stage at which what you ask for is done (instead of maximising it
+   in order to maximise parallelism of the build process).
+
+   For example, if you only want to test whether bin/coqtop still
+   builds (and eventually start it to test your bugfix or new
+   feature), don't do "make world" and interrupt it when bin/coqtop is
+   built. Use "make bin/coqtop" or "make coqbinaries" or something
+   like that. This will avoid entering the stage 3, and cut build
+   system overhead by 50% (1.2s instead of 2.4 on writer's machine).
+
+ - You can turn off rebuilding of the standard library each time
+   bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1.
+
+ - If you want to avoid all .ml4 files being recompiled only because
+   grammar.cma was rebuilt, do "make ml4depclean" once and then use
+   NO_RECOMPILE_ML4=1.
+
+ - The CM_STAGE1=1 option to make will build all .cm* files mentioned
+   as targets on the command line in stage1. Whether this will work is
+   your responsibility. It should work for .ml files that don't depend
+   (nor directly nor indirectly through transitive closure of the
+   dependencies) on any .ml4 file, or where those dependencies can be
+   safely ignored in the current situation (e.g. all these .ml4 files
+   don't need to be recompiled).
+
+   This will avoid entering the stage2 (a reduction of 33% in
+   overhead, 0.4s on the writer's machine).
+
+ - To jump directly into a stage (e.g. because you know nothing is to
+   be done in stage 1 or (1 and 2) or because you know that the target
+   you give can be, in this situation, done in a lower stage than the
+   build system dares to), use GOTO_STAGE=n. This will jump into stage
+   n and try to do the targets you gave in that stage.
+
+ - To disable all dependency recalculation, use the NO_RECALC_DEPS=1
+   option. It disables REcalculation of dependencies, not calculation
+   of dependencies. In other words, if a .d file does not exist, it is
+   still created, but it is not updated every time the source file
+   (e.g. .ml) is changed.
+
+General speed improvements:
+
+ - When building both the native and bytecode versions, the
+   KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time
+   by running camlp4o only once on every .ml4 file, at the expense of
+   readability of compilation error messages for .ml4 files.
+
+Dependencies
+------------
+
+There are no dependencies in the archive anymore, they are always
+bootstrapped. The dependencies of a file FOO are in FOO.d . This
+enables partial recalculation of dependencies (only the dependencies
+of changed files are recomputed).
+
+If you add a dependency to a Coq camlp4 extension (grammar.cma or
+q_constr.cmo), then see sections ".ml4 files" and "new files".
+
+Cleaning Targets
+----------------
+
+Targets for cleaning various parts:
+
+ - distclean: clean everything; must leave only what should end up in
+   distribution tarball and/or is in a svn checkout.
+
+ - clean: clean everything except effect of "./configure" and documentation.
+
+ - cleanconfig: clean effect of "./configure" only
+
+ - archclean:  remove all architecture-dependent   generated files
+ - indepclean: remove all architecture-independent generated files
+   (not documentation)
+
+ - objclean: clean all generated files, but not Makefile meta-data
+   (e.g. dependencies), nor debugging/development information nor
+   other cruft (e.g. editor backup files), nor documentation
+
+ - docclean: clean documentation
+
+.ml4 files
+----------
+
+The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and
+can be obtained with:
+ make FOO.ml4-preprocessed
+
+If a .ml4 file uses a grammar extension from Coq (such as grammar.cma
+or q_constr.cmo), it must contain a line like:
+ (*i camlp4deps: "grammar.cma q_constr.cmo" i*)
+
+If it uses a standard grammar extension, it must contain a line like:
+ (*i camlp4use: "pa_ifdef.cmo" i*)
+
+It can naturally contain both a camlp4deps and a camlp4use line. Both
+are used for preprocessing. It is thus _not_ necessary to add a
+specific rule for a .ml4 file in the Makefile.build just because it
+uses grammar extensions.
+
+By default, the build system is geared towards development that may
+use the Coq grammar extensions, but not development of Coq's grammar
+extensions themselves. This means that .ml4 files are compiled
+directly (using ocamlc/opt's -pp option), without use of an
+intermediary .ml (or .ml4-preprocessed) file. This is so that if a
+compilation error occurs, the location in the error message is a
+location in the .ml4 file. If you are modifying the grammar
+extensions, you may be more interested in the location of the error in
+the .ml4-preprocessed file, so that you can see what your new grammar
+extension made wrong. In that case, use the KEEP_ML4_PREPROCESSED=1
+option. This will make compilation of a .ml4 file a two-stage process:
+
+1) create the .ml4-preprocessed file with camlp4o
+2) compile it with straight ocamlc/opt without preprocessor
+
+and will instruct make not to delete .ml4-preprocessed files
+automatically just because they are intermediary files, so that you
+can inspect them.
+
+If you add a _new_ grammar extension to Coq:
+
+ - if it can be built at stage1, that is the .ml4 file does not use a
+   Coq grammar extension itself, then add it, and all .cmo files it
+   needs to STAGE1_TARGETS and STAGE_ML4 in Makefile.common. See the
+   handling of grammar.cma and q_constr.cmo for an example.
+
+ - if it cannot be built at stage1, that is the .ml4 file itself needs
+   to be preprocessed with a Coq camlp4 grammar extension, then,
+   congratulations, you need to add a new stage between stage1 and
+   stage2.
+
+New files
+---------
+
+For a new file, in most cases, you just have to add it to the proper
+file list(s) in Makefile.common, such as ARITHVO or TACTICS.
+
+The list of all ml4 files is not handled manually anymore.
+
+Exceptions are:
+
+ - The file is necessary at stage1, that it is necessary to build the
+   Coq camlp4 grammar extensions. In this case, make sure it ends up
+   in STAGE1_CMO and (for .ml4 files) STAGE1_ML4. See the handling of
+   grammar.cma and/or q_constr.cmo for an example.
+
+ - if the file needs to be compiled with -rectypes, add it to
+   RECTYPESML in Makefile.common. If it is a .ml4 file, implement
+   RECTYPESML4 or '(*i ocamlflags i*)'; see TODO.
+
+ - the file needs a specific Makefile entry; add it to Makefile.build
+
+ - the files produced from the added file do not match an existing
+   pattern or entry in "Makefile". (All the common cases of
+   .ml{,i,l,y,4}, .v, .c, ... files that produces (respectively)
+   .cm[iox], .vo, .glob, .o, ... files with the same basename are
+   already covered.) In this case, see section "New targets".
+
+New targets
+-----------
+
+If you want to add:
+
+ - a new PHONY target to the build system, that is a target that is
+   not the name of the file it creates,
+
+ - a normal target is not already mapped to a stage by "Makefile"
+
+ then:
+
+ - add the necessary rule to Makefile.build, if any
+ - add the target to STAGEn_TARGETS, with n being the smallest stage
+   it can be built at, that is:
+   * 1 for OCaml code that doesn't use any Coq camlp4 grammar extension
+   * 2 for OCaml code that uses (directly or indirectly) a Coq
+       camlp4 grammar extension. Indirectly means a dependency of it
+       does.
+   * 3 for Coq (.v) code.
+
+   *or*
+
+   add a pattern matching the target to the pattern lists for the
+   smallest stage it can be built at in "Makefile".
+
+TODO
+----
+
+delegate pa_extend.cmo to camlp4use statements and remove it from
+standard camlp4 options.
+
+maybe manage compilation flags (such as -rectypes or the CoqIDE ones)
+from a
+ (*i ocamlflags: "-rectypes" i*)
+statement in the .ml(4) files themselves, like camlp4use. The CoqIDE
+files could have
+ (*i ocamlflags: "${COQIDEFLAGS}" i*)
+and COQIDEFLAGS is still defined (and exported by) the Makefile.build.
+
+Clean up doc/Makefile
+
+config/Makefile looks like it contains a lot of unused variables,
+clean that up (are any maybe used by nightly scripts on
+pauillac?). Also, the COQTOP variable from config/Makefile (and used
+in contribs) has a very poorly chosen name, because "coqtop" is the
+name of a Coq executable! For example, in the Coq makefile it is
+immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or
+COQTREE or COQDIR or ...
+
+Promote the granular .glob handling to official way of doing things
+for Coq developments, that is implement it in coq_makefile and the
+contribs. Here are a few hints:
+
+>> Les fichiers de constantes produits par -dump-glob sont maintenant
+>> produits par fichier et sont ensuite concaténés dans
+>> glob.dump. Ilsont produits par défaut (avec les bonnes
+>> dépendances).
+
+> C'est une chose que l'on voulait faire aussi.
+
+(J'ai testé et débogué ce concept sur CoRN dans les derniers mois.)
+
+> Est-ce que vous sauriez modifier coq_makefile pour qu'il procède de
+> la même façon
+
+Dans cette optique, il serait alors plus propre de changer coqdep pour
+qu'il produise directement l'output que nous mettons maintenant dans
+les .v.d (qui est celui de coqdoc post-processé avec sed).
+
+Si cette manière de gérer les glob devient le standard béni
+officiellement par "the Coq development team", ne voudrions nous pas
+changer coqc pour qu'il produise FOO.glob lors de la compilation de
+FOO.v par défaut (sans argument "-dump-glob")?
+
+> et que la production de a.html par coqdoc n'ait une dépendance qu'en
+> les a.v et a.glob correspondant ?
+
+Je crois que coqdoc exige un glob-dump unique, il convient donc de
+concaténer les .glob correspondants. Soit un glob-dump global par
+projet (par Makefile), soit un glob-dump global par .v(o), qui
+contient son .glob et ceux de tous les .v(o) atteignables par le
+graphe des dépendances. CoRN contient déjà un outil de calcul de
+partie atteignable du graphe des dépendances (il y est pour un autre
+usage, pour calculer les .v à mettre dans les différents tarballs sur
+http://corn.cs.ru.nl/download.html; les parties partielles sont
+définies par liste de fichiers .v + toutes leurs dépendances
+(in)directes), il serait alors adéquat de le mettre dans les tools de
+Coq.
+
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 90e29496..b7545e09 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,37 @@
 =========================================
+= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
+=========================================
+
+A few differences in Coq ML interfaces between Coq V8.1 and V8.2
+================================================================
+
+** Datatypes
+
+List of occurrences moved from "int list" to "Termops.occurrences" (an
+alias to "bool * int list").
+
+** Functions
+
+Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
+Tactics: apply_with_bindings -> apply_with_bindings_wo_evars
+Eauto.simplest_apply -> Hiddentac.h_simplest_apply
+Evarutil.define_evar_as_arrow -> define_evar_as_product
+
+** Universe names (univ.mli)
+
+ base_univ -> type0_univ  (* alias of Set is the Type hierarchy *)
+ prop_univ -> type1_univ  (* the type of Set in the Type hierarchy *)
+ neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *)
+ is_base_univ -> is_type1_univ
+ is_empty_univ -> is_lower_univ
+
+** Sort names (term.mli)
+
+  mk_Set -> set_sort
+  mk_Prop -> prop_sort
+  type_0 -> type1_sort
+
+=========================================
 = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
 =========================================
 
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion
new file mode 100644
index 00000000..6274275c
--- /dev/null
+++ b/dev/doc/notes-on-conversion
@@ -0,0 +1,73 @@
+(**********************************************************************)
+(* A few examples showing the current limits of the conversion algorithm *)
+(**********************************************************************)
+
+(*** We define (pseudo-)divergence from Ackermann function ***)
+
+Definition ack (n : nat) :=
+  (fix F (n0 : nat) : nat -> nat :=
+     match n0 with
+     | O => S
+     | S n1 =>
+         fun m : nat =>
+         (fix F0 (n2 : nat) : nat :=
+            match n2 with
+            | O => F n1 1
+            | S n3 => F n1 (F0 n3)
+            end) m
+     end) n.
+
+Notation OMEGA := (ack 4 4).
+
+Definition f (x:nat) := x.
+
+(* Evaluation in tactics can somehow be controled *)
+Lemma l1 : OMEGA = OMEGA.
+reflexivity.  (* succeed: identity *)
+Qed.          (* succeed: identity *)
+
+Lemma l2 : OMEGA = f OMEGA.
+reflexivity.  (* fail: conversion wants to convert OMEGA with f OMEGA *)
+Abort.        (* but it reduces the right side first! *)
+
+Lemma l3 : f OMEGA = OMEGA.
+reflexivity.  (* succeed: reduce left side first *)
+Qed.          (* succeed: expected concl (the one with f) is on the left *)
+
+Lemma l4 : OMEGA = OMEGA.
+assert (f OMEGA = OMEGA) by reflexivity. (* succeed *)
+unfold f in H.   (* succeed: no type-checking *)
+exact H.         (* succeed: identity *)
+Qed.             (* fail: "f" is on the left *)
+
+(* This example would fail whatever the preferred side is *)
+Lemma l5 : OMEGA = f OMEGA.
+unfold f.
+assert (f OMEGA = OMEGA) by reflexivity.
+unfold f in H.
+exact H.
+Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *)
+
+(**********************************************************************)
+(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *)
+(* (proof of span_ind_uninject_prop *)
+
+In the proof, a problem of the form   (Equal S t1 t2)
+is "simpl"ified, then "red"uced to    (Equal S' t1 t1)
+where the new t1's are surrounded by invisible coercions.
+A reflexivity steps conclude the proof.
+
+The trick is that Equal projects the equality in the setoid S, and
+that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)).
+
+At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1)
+and the algorithm is to first compare S and S', and t1 and t2.
+Unfortunately it does not work, and since t1 and t2 involve concrete
+instances of algebraic structures, it takes a lot of time to realize that
+it is not convertible.
+
+The only hope to improve this problem is to observe that S' hides
+(behind two indirections) a Setoid constructor. This could be the
+argument to solve the problem.
+
+
diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index f4cb3bff..8e481544 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,13 +1,79 @@
-Performance analysis for V8-0 branch
-------------------------------------
+Performance analysis (trunk repository)
+---------------------------------------
 
-Oct 29, 2006: polymorphism on definitions (+ 4%)
+May 21, 2008: New version of CoRN
+  (needs +84% more time to compile)
+
+Apr 25-29, 2008: Temporary attempt with delta in eauto (Matthieu)
+  (+28% CoRN) 
+
+Apr 17, 2008: improvement probably due to commit 10807 or 10813 (bug
+  fixes, control of zeta in rewrite, auto (??))
+  (-18% Buchberger, -40% PAutomata, -28% IntMap, -43% CoRN, -13% LinAlg,
+  but CatsInZFC -0.5% only, PiCalc stable, PersistentUnionFind -1%)
+
+Mar 11, 2008:
+  (+19% PersistentUnionFind wrt Mar 3, +21% Angles, 
+   +270% Continuations between 7/3 and 18/4)
+
+Mar 7, 2008:
+  (-10% PersistentUnionFind wrt Mar 3)
+
+Feb 20, 2008: temporary 1-day slow down
+  (+64% LinAlg)
+
+Feb 14, 2008:
+  (-10% PersistentUnionFind, -19% Groups)
+
+Feb 7, 8, 2008: temporary 2-days long slow down
+  (+20 LinAlg, +50% BDDs)
+
+Feb 2, 2008: many updates of the module system
+  (-13% LinAlg, -50% AMM11262, -5% Goedel, -1% PersistentUnionFind, 
+   -42% ExactRealArithmetic, -41% Icharate, -42% Kildall, -74% SquareMatrices)
+
+Jan 1, 2008: merge of TypeClasses branch
+  (+8% PersistentUnionFind, +36% LinAlg, +76% Goedel)
+
+Nov 16, 17, 2007:
+  (+18% Cantor, +4% LinAlg, +27% IEEE1394 on 2 days)
+
+Nov 8, 2007:
+  (+18% Cantor, +16% LinAlg, +55% Continuations, +200% IEEE1394, +170% CTLTCTL,
+   +220% SquareMatrices)
+
+Oct 29, V8.1 (+ 3% geometry but CoRN, Godel, Kildall, Stalmark stables)
+
+Between Oct 12 and Oct 27, 2007: inefficiency temporarily introduced in the
+  tactic interpreter (from revision 10222 to 10267)
+  (+22% CoRN, +10% geometry, ...)
+
+Sep 16, 2007:
+  (+16% PersistentUnionFind on 3 days, LinAlg stable,
+
+Sep 4, 2007:
+  (+26% PersistentUnionFind, LinAlg stable,
+
+Jun 6, 2007: optimization of the need for type unification in with-bindings
+  (-3.5% Stalmark, -6% Kildall)
+
+May 20, 21, 22, 2007: improved inference of with-bindings (including activation
+  of unification on types)
+  (+4% PICALC, +5% Stalmark, +7% Kildall)
+
+May 11, 2007: added primitive integers (+6% CoLoR, +7% CoRN, +5% FSets, ...)
+
+Between Feb 22 and March 16, 2007: bench temporarily moved on JMN's
+  computer (-25% CoRN, -25% Fairisle, ...)
+
+Oct 29 and Oct 30, 2006: abandoned attempt to add polymorphism on definitions
+  (+4% in general during these two days)
 
 Oct 17, 2006: improvement in new field [r9248]
   (QArith -3%, geometry: -2%)
 
 Oct 5, 2006: fixing wrong unification of Meta below binders
-  (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, 
+  (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, LinAlg: +7%,
    DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%)
 
 Sep 26, 2006: new field [r9178-9181]
@@ -17,11 +83,17 @@ Sep 26, 2006: new field [r9178-9181]
   Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s)
   May 30, 2006: Nancy/CoLoR added (~ 319s)
 
+May 23, 2006: new, lighter version of polymorphic inductive types
+  (CoRN: -27%, back to Mar-24 time)
+
 May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -)
 
 May 5, 2006: improvement in closure (array instead of lists)
   (e.g. CatsInZFC: -10%, CoRN: -3%, 
 
+May 23, 2006: polymorphic inductive types (precise, heavy algorithm)
+  (CoRN: +37%)
+
   Dec 29, 2005: new test and use of -vm in Stalmarck
 
   Dec 27, 2005: contrib Karatsuba added (~ 30s)
diff --git a/dev/doc/header b/dev/header
index 57945e47..57945e47 100644
--- a/dev/doc/header
+++ b/dev/header
diff --git a/dev/include b/dev/include
index 42d2a017..ccb75edd 100644
--- a/dev/include
+++ b/dev/include
@@ -1,9 +1,17 @@
 
 (* File to include to install the pretty-printers in the ocaml toplevel *)
 
+(* clflags.cmi (a ocaml compilation by-product) must be in the library path.
+   On Debian, install ocaml-compiler-libs, and uncomment the following:
+   #directory "+compiler-libs/utils";;
+*)
+
+(* Clflags.recursive_types := true;;*)
 #cd ".";;
 #use "base_include";;
 
+#install_printer  (* pp_stdcmds *) pppp;;
+
 #install_printer  (* pattern *) pppattern;;
 #install_printer  (* rawconstr *) pprawconstr;;
 
@@ -17,6 +25,7 @@
 #install_printer  (* goal *)  ppgoal;;
 #install_printer  (* sigma goal *)  ppsigmagoal;;
 #install_printer  (* proof *)  pproof;;
+#install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
 #install_printer  (* evar_defs *)  ppevd;;
 #install_printer  (* clenv *) ppclenv;;
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 2d1c6289..ac5ec1e0 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -6,15 +6,12 @@ export COQTOP=COQTOPDIRECTORY
 export COQLIB=COQLIBDIRECTORY
 export COQTH=$COQLIB/theories
 CAMLBIN=CAMLBINDIRECTORY
+CAMLP4LIB=CAMLP4LIBDIRECTORY
 OCAMLDEBUG=$CAMLBIN/ocamldebug
-if [ -x "$CAMLBIN/camlp5" ]; then 
-  export CAMLP4LIB=`$CAMLBIN/camlp5 -where`
-else
-  export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
-fi
 
 exec $OCAMLDEBUG \
 	-I $CAMLP4LIB \
+	-I $COQTOP \
 	-I $COQTOP/config \
 	-I $COQTOP/lib -I $COQTOP/kernel \
 	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
@@ -22,7 +19,7 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
 	-I $COQTOP/translate \
         -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
-        -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/first-order \
+        -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/firstorder \
         -I $COQTOP/contrib/interface  -I $COQTOP/contrib/jprover \
         -I $COQTOP/contrib/omega      -I $COQTOP/contrib/romega \
         -I $COQTOP/contrib/ring       -I $COQTOP/contrib/xml \
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile
index 96491017..7ab1bd3f 100644
--- a/dev/ocamlweb-doc/Makefile
+++ b/dev/ocamlweb-doc/Makefile
@@ -1,5 +1,20 @@
+include ../../config/Makefile
+
+LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \
+	      -I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \
+              -I ../../proofs -I ../../tactics -I ../../pretyping \
+              -I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \
+              -I ../../contrib/omega -I ../../contrib/romega \
+	      -I ../../contrib/ring -I ../../contrib/dp -I ../../contrib/setoid_ring \
+              -I ../../contrib/xml -I ../../contrib/extraction \
+              -I ../../contrib/interface -I ../../contrib/fourier \
+	      -I ../../contrib/jprover -I ../../contrib/cc \
+	      -I ../../contrib/funind -I ../../contrib/firstorder \
+              -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \
+              -I ../../contrib/recdef
+
+MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
-# Makefile for doc/
 
 all:: newparse coq.ps minicop.ps
 #newsyntax.dvi minicoq.dvi
@@ -55,8 +70,8 @@ coq.tex::
 depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \
          proofs.dep.ps tactics.dep.ps toplevel.dep.ps interp.dep.ps
 
-%.dot: ../%
-	(cd ../$*; ocamldep *.ml *.mli) | ocamldot -lr > $@
+%.dot: ../../%
+	ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../../$*/*.ml ../../$*/*.mli -o $@
 
 %.dep.ps: %.dot
 	dot -Tps $< -o $@
diff --git a/dev/ocamlweb-doc/interp.dep.ps b/dev/ocamlweb-doc/interp.dep.ps
index b0554481..fda7a33c 100644
--- a/dev/ocamlweb-doc/interp.dep.ps
+++ b/dev/ocamlweb-doc/interp.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
-%%For: (herbelin) Hugo Herbelin
+%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
+%%For: (notin) Jean-Marc Notin,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 35 35 577 160
+%%BoundingBox: (atend)
 %%EndComments
 save
 %%BeginProlog
@@ -16,57 +16,7 @@ mark
  EncodingVector 0
 
 ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
-  dup 306 /AE
-  dup 301 /Aacute
-  dup 302 /Acircumflex
-  dup 304 /Adieresis
-  dup 300 /Agrave
-  dup 305 /Aring
-  dup 303 /Atilde
-  dup 307 /Ccedilla
-  dup 311 /Eacute
-  dup 312 /Ecircumflex
-  dup 313 /Edieresis
-  dup 310 /Egrave
-  dup 315 /Iacute
-  dup 316 /Icircumflex
-  dup 317 /Idieresis
-  dup 314 /Igrave
-  dup 334 /Udieresis
-  dup 335 /Yacute
-  dup 376 /thorn
-  dup 337 /germandbls
-  dup 341 /aacute
-  dup 342 /acircumflex
-  dup 344 /adieresis
-  dup 346 /ae
-  dup 340 /agrave
-  dup 345 /aring
-  dup 347 /ccedilla
-  dup 351 /eacute
-  dup 352 /ecircumflex
-  dup 353 /edieresis
-  dup 350 /egrave
-  dup 355 /iacute
-  dup 356 /icircumflex
-  dup 357 /idieresis
-  dup 354 /igrave
-  dup 360 /dcroat
-  dup 361 /ntilde
-  dup 363 /oacute
-  dup 364 /ocircumflex
-  dup 366 /odieresis
-  dup 362 /ograve
-  dup 365 /otilde
-  dup 370 /oslash
-  dup 372 /uacute
-  dup 373 /ucircumflex
-  dup 374 /udieresis
-  dup 371 /ugrave
-  dup 375 /yacute
-  dup 377 /ydieresis  
+EncodingVector 45 /hyphen put
 
 % Set up ISO Latin 1 character encoding
 /starnetISO {
@@ -98,8 +48,8 @@ cleartomark
 
 /InvScaleFactor 1.0 def
 /set_scale {
-	dup 1 exch div /InvScaleFactor exch def
-	dup scale
+       dup 1 exch div /InvScaleFactor exch def
+       scale
 } bind def
 
 % styles
@@ -229,348 +179,359 @@ def
 } if
 
 %%EndSetup
+setupLatin1
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 160
-%%PageOrientation: Portrait
+%%PageBoundingBox: 36 36 576 753
+%%PageOrientation: Landscape
 gsave
-35 35 542 125 boxprim clip newpath
-36 36 translate
+36 36 576 753 boxprim clip newpath
 0 0 1 beginpage
-0.9343 set_scale
-0 0 translate 0 rotate
-0.000 0.000 0.000 graphcolor
+0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate
+0.000 0.000 1.000 graphcolor
+newpath -4 -4 moveto
+-4 544 lineto
+724 544 lineto
+724 -4 lineto
+closepath fill
+0.985401 setlinewidth
+0.000 0.000 1.000 graphcolor
+newpath -4 -4 moveto
+-4 544 lineto
+724 544 lineto
+724 -4 lineto
+closepath stroke
+% Constrextern
+gsave
+0.502 1.000 0.820 nodecolor
+172 417 49.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+172 417 49.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
 14.00 /Times-Roman set_font
-
-%	Syntax_def
-gsave 10 dict begin
-303 110 45 18 ellipse_path
-stroke
-gsave 10 dict begin
-271 105 moveto
-(Syntax_def)
-[7.68 6.96 6.96 4.08 6.24 6.96 6.96 6.96 6.24 4.56]
-xshow
-end grestore
-end grestore
-
-%	Notation
-gsave 10 dict begin
-422 60 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-397 55 moveto
-(Notation)
-[9.84 6.72 4.08 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Syntax_def -> Notation
-newpath 334 97 moveto
-350 90 369 83 385 76 curveto
+172 412 moveto 72 -0.5 (Constrextern) alignedtext
+grestore
+% Reserve
+gsave
+0.502 1.000 0.820 nodecolor
+264 319 35.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+264 319 35.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+264 314 moveto 44 -0.5 (Reserve) alignedtext
+grestore
+% Constrextern->Reserve
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 188 400 moveto
+203 384 225 361 242 343 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 245.049 344.831 moveto
+249 335 lineto
+239.781 340.221 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 386 79 moveto
-394 72 lineto
-383 73 lineto
-closepath
-fill
+newpath 245.049 344.831 moveto
+249 335 lineto
+239.781 340.221 lineto
+closepath stroke
+grestore
+% Notation
+gsave
+0.502 1.000 0.820 nodecolor
+268 122 37.1753 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+268 122 37.1753 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+268 117 moveto 49 -0.5 (Notation) alignedtext
+grestore
+% Constrextern->Notation
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 386 79 moveto
-394 72 lineto
-383 73 lineto
-closepath
-stroke
-end grestore
-
-%	Ppextend
-gsave 10 dict begin
-537 60 39 18 ellipse_path
+newpath 178 399 moveto
+194 349 240 209 259 150 curveto
 stroke
-gsave 10 dict begin
-511 55 moveto
-(Ppextend)
-[7.68 6.96 5.76 6.96 3.84 6.24 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Notation -> Ppextend
-newpath 460 60 moveto
-469 60 478 60 488 60 curveto
-stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 262.479 150.584 moveto
+262 140 lineto
+255.774 148.573 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 488 64 moveto
-498 60 lineto
-488 57 lineto
-closepath
-fill
+newpath 262.479 150.584 moveto
+262 140 lineto
+255.774 148.573 lineto
+closepath stroke
+grestore
+% Topconstr
+gsave
+0.502 1.000 0.820 nodecolor
+82 24 41.1755 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+82 24 41.1755 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+82 19 moveto 57 -0.5 (Topconstr) alignedtext
+grestore
+% Notation->Topconstr
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 488 64 moveto
-498 60 lineto
-488 57 lineto
-closepath
-stroke
-end grestore
-
-%	Topconstr
-gsave 10 dict begin
-537 114 41 18 ellipse_path
+newpath 243 109 moveto
+211 91 154 62 117 43 curveto
 stroke
-gsave 10 dict begin
-509 109 moveto
-(Topconstr)
-[7.2 6.96 6.96 6.24 6.96 6.96 5.28 3.84 4.56]
-xshow
-end grestore
-end grestore
-
-%	Notation -> Topconstr
-newpath 449 73 moveto
-464 80 483 89 500 97 curveto
-stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 118.441 39.7969 moveto
+108 38 lineto
+115.042 45.916 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 498 100 moveto
-509 101 lineto
-501 94 lineto
-closepath
-fill
+newpath 118.441 39.7969 moveto
+108 38 lineto
+115.042 45.916 lineto
+closepath stroke
+grestore
+% Ppextend
+gsave
+0.502 1.000 0.820 nodecolor
+278 24 39.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+278 24 39.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+278 19 moveto 52 -0.5 (Ppextend) alignedtext
+grestore
+% Notation->Ppextend
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 498 100 moveto
-509 101 lineto
-501 94 lineto
-closepath
-stroke
-end grestore
-
-%	Modintern
-gsave 10 dict begin
-44 98 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-13 93 moveto
-(Modintern)
-[12.48 6.96 6.96 3.84 6.96 3.84 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-%	Constrintern
-gsave 10 dict begin
-173 98 48 18 ellipse_path
+newpath 270 104 moveto
+272 89 273 68 275 52 curveto
 stroke
-gsave 10 dict begin
-138 93 moveto
-(Constrintern)
-[9.36 6.96 6.96 5.28 3.84 4.8 3.84 6.96 3.84 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-%	Modintern -> Constrintern
-newpath 88 98 moveto
-97 98 106 98 115 98 curveto
-stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 278.488 52.2987 moveto
+276 42 lineto
+271.522 51.6021 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 115 102 moveto
-125 98 lineto
-115 95 lineto
-closepath
-fill
+newpath 278.488 52.2987 moveto
+276 42 lineto
+271.522 51.6021 lineto
+closepath stroke
+grestore
+% Constrintern
+gsave
+0.502 1.000 0.820 nodecolor
+472 417 48.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+472 417 48.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+472 412 moveto 70 -0.5 (Constrintern) alignedtext
+grestore
+% Constrintern->Reserve
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 115 102 moveto
-125 98 lineto
-115 95 lineto
-closepath
-stroke
-end grestore
-
-%	Constrintern -> Syntax_def
-newpath 220 102 moveto
-229 103 239 104 249 105 curveto
+newpath 442 403 moveto
+404 385 340 355 299 335 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 300.56 331.863 moveto
+290 331 lineto
+297.717 338.26 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 249 108 moveto
-259 106 lineto
-249 102 lineto
-closepath
-fill
+newpath 300.56 331.863 moveto
+290 331 lineto
+297.717 338.26 lineto
+closepath stroke
+grestore
+% Implicit_quantifiers
+gsave
+0.502 1.000 0.820 nodecolor
+508 319 69.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+508 319 69.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+508 314 moveto 112 -0.5 (Implicit_quantifiers) alignedtext
+grestore
+% Constrintern->Implicit_quantifiers
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 249 108 moveto
-259 106 lineto
-249 102 lineto
-closepath
+newpath 479 399 moveto
+484 385 492 364 498 347 curveto
 stroke
-end grestore
-
-%	Reserve
-gsave 10 dict begin
-303 56 35 18 ellipse_path
-stroke
-gsave 10 dict begin
-280 51 moveto
-(Reserve)
-[9.12 6.24 5.52 6.24 4.8 6.48 6.24]
-xshow
-end grestore
-end grestore
-
-%	Constrintern -> Reserve
-newpath 210 86 moveto
-227 81 246 75 263 69 curveto
-stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 501.479 347.584 moveto
+501 337 lineto
+494.774 345.573 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 264 72 moveto
-273 66 lineto
-262 66 lineto
-closepath
-fill
+newpath 501.479 347.584 moveto
+501 337 lineto
+494.774 345.573 lineto
+closepath stroke
+grestore
+% Syntax_def
+gsave
+0.502 1.000 0.820 nodecolor
+396 220 45.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+396 220 45.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+396 215 moveto 64 -0.5 (Syntax_def) alignedtext
+grestore
+% Implicit_quantifiers->Syntax_def
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 264 72 moveto
-273 66 lineto
-262 66 lineto
-closepath
-stroke
-end grestore
-
-%	Genarg
-gsave 10 dict begin
-422 114 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-401 109 moveto
-(Genarg)
-[10.08 6.24 6.96 6.24 4.32 6.96]
-xshow
-end grestore
-end grestore
-
-%	Genarg -> Topconstr
-newpath 456 114 moveto
-465 114 476 114 486 114 curveto
+newpath 488 302 moveto
+469 285 442 261 422 244 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 424.546 241.596 moveto
+415 237 lineto
+419.596 246.546 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 486 118 moveto
-496 114 lineto
-486 111 lineto
-closepath
-fill
+newpath 424.546 241.596 moveto
+415 237 lineto
+419.596 246.546 lineto
+closepath stroke
+grestore
+% Coqlib
+gsave
+0.502 1.000 0.820 nodecolor
+656 515 32.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+656 515 32.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+656 510 moveto 38 -0.5 (Coqlib) alignedtext
+grestore
+% Genarg
+gsave
+0.502 1.000 0.820 nodecolor
+82 122 33.175 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+82 122 33.175 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+82 117 moveto 41 -0.5 (Genarg) alignedtext
+grestore
+% Genarg->Topconstr
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 486 118 moveto
-496 114 lineto
-486 111 lineto
-closepath
-stroke
-end grestore
-
-%	Coqlib
-gsave 10 dict begin
-44 21 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-24 16 moveto
-(Coqlib)
-[9.36 6.96 6.96 3.84 3.84 6.96]
-xshow
-end grestore
-end grestore
-
-%	Constrextern
-gsave 10 dict begin
-173 21 49 18 ellipse_path
+newpath 82 104 moveto
+82 89 82 69 82 52 curveto
 stroke
-gsave 10 dict begin
-137 16 moveto
-(Constrextern)
-[9.36 6.96 6.96 5.28 3.84 4.56 5.76 6.96 3.84 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-%	Coqlib -> Constrextern
-newpath 77 21 moveto
-88 21 101 21 114 21 curveto
-stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 85.5001 52 moveto
+82 42 lineto
+78.5001 52 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 114 25 moveto
-124 21 lineto
-114 18 lineto
-closepath
-fill
+newpath 85.5001 52 moveto
+82 42 lineto
+78.5001 52 lineto
+closepath stroke
+grestore
+% Syntax_def->Notation
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 114 25 moveto
-124 21 lineto
-114 18 lineto
-closepath
-stroke
-end grestore
-
-%	Constrextern -> Notation
-newpath 222 19 moveto
-257 18 307 20 348 29 curveto
-361 31 375 37 388 42 curveto
+newpath 375 204 moveto
+354 187 320 161 296 143 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 298.1 140.2 moveto
+288 137 lineto
+293.9 145.8 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 386 45 moveto
-397 46 lineto
-389 39 lineto
-closepath
-fill
+newpath 298.1 140.2 moveto
+288 137 lineto
+293.9 145.8 lineto
+closepath stroke
+grestore
+% Modintern
+gsave
+0.502 1.000 0.820 nodecolor
+472 515 42.1756 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+472 515 42.1756 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+472 510 moveto 59 -0.5 (Modintern) alignedtext
+grestore
+% Modintern->Constrintern
+gsave
+0.985401 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 386 45 moveto
-397 46 lineto
-389 39 lineto
-closepath
+newpath 472 497 moveto
+472 482 472 462 472 445 curveto
 stroke
-end grestore
-
-%	Constrextern -> Reserve
-newpath 213 32 moveto
-228 36 246 41 261 45 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 260 48 moveto
-271 48 lineto
-262 42 lineto
-closepath
-fill
+newpath 475.5 445 moveto
+472 435 lineto
+468.5 445 lineto
+closepath fill
+0.985401 setlinewidth
+solid
 0.000 0.000 0.000 edgecolor
-newpath 260 48 moveto
-271 48 lineto
-262 42 lineto
-closepath
-stroke
-end grestore
+newpath 475.5 445 moveto
+472 435 lineto
+468.5 445 lineto
+closepath stroke
+grestore
 endpage
 showpage
 grestore
@@ -578,6 +539,7 @@ grestore
 %%EndPage: 1
 %%Trailer
 %%Pages: 1
+%%BoundingBox: 36 36 576 753
 end
 restore
 %%EOF
diff --git a/dev/ocamlweb-doc/kernel.dep.ps b/dev/ocamlweb-doc/kernel.dep.ps
index 3c00121e..b7b4137b 100644
--- a/dev/ocamlweb-doc/kernel.dep.ps
+++ b/dev/ocamlweb-doc/kernel.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
-%%For: (herbelin) Hugo Herbelin
+%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
+%%For: (notin) Jean-Marc Notin,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 35 35 577 127
+%%BoundingBox: (atend)
 %%EndComments
 save
 %%BeginProlog
@@ -16,57 +16,7 @@ mark
  EncodingVector 0
 
 ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
-  dup 306 /AE
-  dup 301 /Aacute
-  dup 302 /Acircumflex
-  dup 304 /Adieresis
-  dup 300 /Agrave
-  dup 305 /Aring
-  dup 303 /Atilde
-  dup 307 /Ccedilla
-  dup 311 /Eacute
-  dup 312 /Ecircumflex
-  dup 313 /Edieresis
-  dup 310 /Egrave
-  dup 315 /Iacute
-  dup 316 /Icircumflex
-  dup 317 /Idieresis
-  dup 314 /Igrave
-  dup 334 /Udieresis
-  dup 335 /Yacute
-  dup 376 /thorn
-  dup 337 /germandbls
-  dup 341 /aacute
-  dup 342 /acircumflex
-  dup 344 /adieresis
-  dup 346 /ae
-  dup 340 /agrave
-  dup 345 /aring
-  dup 347 /ccedilla
-  dup 351 /eacute
-  dup 352 /ecircumflex
-  dup 353 /edieresis
-  dup 350 /egrave
-  dup 355 /iacute
-  dup 356 /icircumflex
-  dup 357 /idieresis
-  dup 354 /igrave
-  dup 360 /dcroat
-  dup 361 /ntilde
-  dup 363 /oacute
-  dup 364 /ocircumflex
-  dup 366 /odieresis
-  dup 362 /ograve
-  dup 365 /otilde
-  dup 370 /oslash
-  dup 372 /uacute
-  dup 373 /ucircumflex
-  dup 374 /udieresis
-  dup 371 /ugrave
-  dup 375 /yacute
-  dup 377 /ydieresis  
+EncodingVector 45 /hyphen put
 
 % Set up ISO Latin 1 character encoding
 /starnetISO {
@@ -98,8 +48,8 @@ cleartomark
 
 /InvScaleFactor 1.0 def
 /set_scale {
-	dup 1 exch div /InvScaleFactor exch def
-	dup scale
+       dup 1 exch div /InvScaleFactor exch def
+       scale
 } bind def
 
 % styles
@@ -229,1219 +179,1245 @@ def
 } if
 
 %%EndSetup
+setupLatin1
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 127
-%%PageOrientation: Portrait
+%%PageBoundingBox: 36 36 535 756
+%%PageOrientation: Landscape
 gsave
-35 35 542 92 boxprim clip newpath
-36 36 translate
+36 36 535 756 boxprim clip newpath
 0 0 1 beginpage
-0.2845 set_scale
-0 0 translate 0 rotate
-0.000 0.000 0.000 graphcolor
+0.393658 0.393658 set_scale 90 rotate 95.45 -1355.45 translate
+0.000 0.000 1.000 graphcolor
+newpath -4 -4 moveto
+-4 1264 lineto
+1825 1264 lineto
+1825 -4 lineto
+closepath fill
+0.393658 setlinewidth
+0.000 0.000 1.000 graphcolor
+newpath -4 -4 moveto
+-4 1264 lineto
+1825 1264 lineto
+1825 -4 lineto
+closepath stroke
+% Cbytecodes
+gsave
+0.502 1.000 0.820 nodecolor
+1258 234 45.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1258 234 45.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
 14.00 /Times-Roman set_font
-
-%	Vm
-gsave 10 dict begin
-801 294 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-789 289 moveto
-(Vm)
-[10.08 10.8]
-xshow
-end grestore
-end grestore
-
-%	Cemitcodes
-gsave 10 dict begin
-1427 200 46 18 ellipse_path
-stroke
-gsave 10 dict begin
-1393 195 moveto
-(Cemitcodes)
-[9.36 6.24 10.8 3.84 3.84 6.24 6.96 6.96 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Vm -> Cemitcodes
-newpath 826 287 moveto
-871 276 969 254 1053 254 curveto
-1053 254 1053 254 1174 254 curveto
-1249 254 1332 231 1382 215 curveto
+1258 229 moveto 64 -0.5 (Cbytecodes) alignedtext
+grestore
+% Term
+gsave
+0.502 1.000 0.820 nodecolor
+1093 162 28.1746 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1093 162 28.1746 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1093 157 moveto 31 -0.5 (Term) alignedtext
+grestore
+% Cbytecodes->Term
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1227 221 moveto
+1198 208 1155 189 1125 176 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1126.56 172.863 moveto
+1116 172 lineto
+1123.72 179.26 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1383 218 moveto
-1392 212 lineto
-1381 212 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1383 218 moveto
-1392 212 lineto
-1381 212 lineto
-closepath
-stroke
-end grestore
-
-%	Conv_oracle
-gsave 10 dict begin
-1053 300 48 18 ellipse_path
-stroke
-gsave 10 dict begin
-1017 295 moveto
-(Conv_oracle)
-[9.36 6.96 6.48 6.96 6.96 6.96 4.56 6.24 6.24 3.84 6.24]
-xshow
-end grestore
-end grestore
-
-%	Vm -> Conv_oracle
-newpath 828 295 moveto
-868 296 942 298 995 299 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1126.56 172.863 moveto
+1116 172 lineto
+1123.72 179.26 lineto
+closepath stroke
+grestore
+% Esubst
+gsave
+0.502 1.000 0.820 nodecolor
+1093 90 31.1748 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1093 90 31.1748 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1093 85 moveto 37 -0.5 (Esubst) alignedtext
+grestore
+% Term->Esubst
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1093 144 moveto
+1093 136 1093 127 1093 118 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1096.5 118 moveto
+1093 108 lineto
+1089.5 118 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 995 303 moveto
-1005 299 lineto
-995 296 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 995 303 moveto
-1005 299 lineto
-995 296 lineto
-closepath
-stroke
-end grestore
-
-%	Mod_subst
-gsave 10 dict begin
-1556 146 45 18 ellipse_path
-stroke
-gsave 10 dict begin
-1524 141 moveto
-(Mod_subst)
-[12.48 6.96 6.96 6.96 5.52 6.96 6.96 5.28 3.84]
-xshow
-end grestore
-end grestore
-
-%	Cemitcodes -> Mod_subst
-newpath 1459 187 moveto
-1476 180 1497 171 1516 163 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1096.5 118 moveto
+1093 108 lineto
+1089.5 118 lineto
+closepath stroke
+grestore
+% Univ
+gsave
+0.502 1.000 0.820 nodecolor
+580 90 27.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+580 90 27.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+580 85 moveto 28 -0.5 (Univ) alignedtext
+grestore
+% Term->Univ
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1065 158 moveto
+979 145 714 109 616 95 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 616.299 91.5125 moveto
+606 94 lineto
+615.602 98.4778 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1517 166 moveto
-1525 159 lineto
-1514 160 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1517 166 moveto
-1525 159 lineto
-1514 160 lineto
-closepath
-stroke
-end grestore
-
-%	Cbytecodes
-gsave 10 dict begin
-1556 200 45 18 ellipse_path
-stroke
-gsave 10 dict begin
-1523 195 moveto
-(Cbytecodes)
-[9.36 6.48 6.96 3.84 6.24 6.24 6.96 6.96 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Cemitcodes -> Cbytecodes
-newpath 1474 200 moveto
-1482 200 1491 200 1500 200 curveto
+0.000 0.000 0.000 edgecolor
+newpath 616.299 91.5125 moveto
+606 94 lineto
+615.602 98.4778 lineto
+closepath stroke
+grestore
+% Cbytegen
+gsave
+0.502 1.000 0.820 nodecolor
+1148 522 39.1754 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1148 522 39.1754 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1148 517 moveto 53 -0.5 (Cbytegen) alignedtext
+grestore
+% Pre_env
+gsave
+0.502 1.000 0.820 nodecolor
+1148 450 36.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1148 450 36.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1148 445 moveto 46 -0.5 (Pre_env) alignedtext
+grestore
+% Cbytegen->Pre_env
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1148 504 moveto
+1148 496 1148 487 1148 478 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 478 moveto
+1148 468 lineto
+1144.5 478 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1500 204 moveto
-1510 200 lineto
-1500 197 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1500 204 moveto
-1510 200 lineto
-1500 197 lineto
-closepath
-stroke
-end grestore
-
-%	Copcodes
-gsave 10 dict begin
-1556 254 41 18 ellipse_path
-stroke
-gsave 10 dict begin
-1528 249 moveto
-(Copcodes)
-[9.36 6.96 6.96 6.24 6.96 6.96 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Cemitcodes -> Copcodes
-newpath 1459 213 moveto
-1476 221 1498 230 1517 237 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 478 moveto
+1148 468 lineto
+1144.5 478 lineto
+closepath stroke
+grestore
+% Declarations
+gsave
+0.502 1.000 0.820 nodecolor
+1148 378 48.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1148 378 48.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1148 373 moveto 70 -0.5 (Declarations) alignedtext
+grestore
+% Pre_env->Declarations
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1148 432 moveto
+1148 424 1148 415 1148 406 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 406 moveto
+1148 396 lineto
+1144.5 406 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1515 240 moveto
-1526 241 lineto
-1518 234 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1515 240 moveto
-1526 241 lineto
-1518 234 lineto
-closepath
-stroke
-end grestore
-
-%	Names
-gsave 10 dict begin
-1865 270 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-1845 265 moveto
-(Names)
-[9.6 6.24 10.8 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Conv_oracle -> Names
-newpath 1102 300 moveto
-1151 300 1228 300 1295 300 curveto
-1295 300 1295 300 1666 300 curveto
-1722 300 1785 288 1825 279 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 406 moveto
+1148 396 lineto
+1144.5 406 lineto
+closepath stroke
+grestore
+% Cemitcodes
+gsave
+0.502 1.000 0.820 nodecolor
+663 306 45.1757 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+663 306 45.1757 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+663 301 moveto 65 -0.5 (Cemitcodes) alignedtext
+grestore
+% Cemitcodes->Cbytecodes
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 706 301 moveto
+813 287 1088 254 1205 240 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1205.4 243.478 moveto
+1215 239 lineto
+1204.7 236.512 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1826 282 moveto
-1835 277 lineto
-1825 276 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1826 282 moveto
-1835 277 lineto
-1825 276 lineto
-closepath
-stroke
-end grestore
-
-%	Vconv
-gsave 10 dict begin
-552 202 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-533 197 moveto
-(Vconv)
-[10.08 6.24 6.96 6.48 6.96]
-xshow
-end grestore
-end grestore
-
-%	Csymtable
-gsave 10 dict begin
-674 202 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-643 197 moveto
-(Csymtable)
-[9.36 5.52 6.96 10.8 4.08 6.24 6.96 3.84 6.24]
-xshow
-end grestore
-end grestore
-
-%	Vconv -> Csymtable
-newpath 584 202 moveto
-595 202 608 202 620 202 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1205.4 243.478 moveto
+1215 239 lineto
+1204.7 236.512 lineto
+closepath stroke
+grestore
+% Copcodes
+gsave
+0.502 1.000 0.820 nodecolor
+786 234 40.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+786 234 40.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+786 229 moveto 54 -0.5 (Copcodes) alignedtext
+grestore
+% Cemitcodes->Copcodes
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 688 291 moveto
+707 281 732 266 752 253 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 753.958 255.916 moveto
+761 248 lineto
+750.559 249.797 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 620 206 moveto
-630 202 lineto
-620 199 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 620 206 moveto
-630 202 lineto
-620 199 lineto
-closepath
-stroke
-end grestore
-
-%	Inductive
-gsave 10 dict begin
-674 110 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-647 105 moveto
-(Inductive)
-[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24]
-xshow
-end grestore
-end grestore
-
-%	Vconv -> Inductive
-newpath 571 187 moveto
-591 172 622 149 645 132 curveto
+0.000 0.000 0.000 edgecolor
+newpath 753.958 255.916 moveto
+761 248 lineto
+750.559 249.797 lineto
+closepath stroke
+grestore
+% Mod_subst
+gsave
+0.502 1.000 0.820 nodecolor
+325 234 43.1756 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+325 234 43.1756 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+325 229 moveto 61 -0.5 (Mod_subst) alignedtext
+grestore
+% Cemitcodes->Mod_subst
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 623 298 moveto
+561 284 441 259 374 244 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 374.492 240.529 moveto
+364 242 lineto
+373.119 247.393 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 647 135 moveto
-653 126 lineto
-643 129 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 647 135 moveto
-653 126 lineto
-643 129 lineto
-closepath
-stroke
-end grestore
-
-%	Csymtable -> Vm
-newpath 696 218 moveto
-717 234 751 258 775 275 curveto
+0.000 0.000 0.000 edgecolor
+newpath 374.492 240.529 moveto
+364 242 lineto
+373.119 247.393 lineto
+closepath stroke
+grestore
+% Mod_subst->Term
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 367 230 moveto
+502 217 925 178 1055 166 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1055.4 169.478 moveto
+1065 165 lineto
+1054.7 162.512 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 773 278 moveto
-783 281 lineto
-777 272 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 773 278 moveto
-783 281 lineto
-777 272 lineto
-closepath
-stroke
-end grestore
-
-%	Cbytegen
-gsave 10 dict begin
-801 164 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-774 159 moveto
-(Cbytegen)
-[9.36 6.48 6.96 3.84 6.24 6.72 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-%	Csymtable -> Cbytegen
-newpath 709 191 moveto
-724 187 742 181 758 177 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1055.4 169.478 moveto
+1065 165 lineto
+1054.7 162.512 lineto
+closepath stroke
+grestore
+% Closure
+gsave
+0.502 1.000 0.820 nodecolor
+713 666 34.1751 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+713 666 34.1751 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+713 661 moveto 43 -0.5 (Closure) alignedtext
+grestore
+% Environ
+gsave
+0.502 1.000 0.820 nodecolor
+1148 594 36.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1148 594 36.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1148 589 moveto 46 -0.5 (Environ) alignedtext
+grestore
+% Closure->Environ
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 746 661 moveto
+823 648 1016 616 1104 602 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1104.88 605.393 moveto
+1114 600 lineto
+1103.51 598.529 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 759 180 moveto
-768 174 lineto
-757 174 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 759 180 moveto
-768 174 lineto
-757 174 lineto
-closepath
-stroke
-end grestore
-
-%	Type_errors
-gsave 10 dict begin
-801 110 47 18 ellipse_path
-stroke
-gsave 10 dict begin
-767 105 moveto
-(Type_errors)
-[6.96 6.96 6.96 6.24 6.96 6.24 5.04 4.56 6.96 4.56 5.52]
-xshow
-end grestore
-end grestore
-
-%	Inductive -> Type_errors
-newpath 714 110 moveto
-724 110 734 110 744 110 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1104.88 605.393 moveto
+1114 600 lineto
+1103.51 598.529 lineto
+closepath stroke
+grestore
+% Environ->Cbytegen
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1148 576 moveto
+1148 568 1148 559 1148 550 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 550 moveto
+1148 540 lineto
+1144.5 550 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 744 114 moveto
-754 110 lineto
-744 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 744 114 moveto
-754 110 lineto
-744 107 lineto
-closepath
-stroke
-end grestore
-
-%	Univ
-gsave 10 dict begin
-1763 241 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-1748 236 moveto
-(Univ)
-[9.6 6.96 3.84 6.96]
-xshow
-end grestore
-end grestore
-
-%	Univ -> Names
-newpath 1788 248 moveto
-1800 251 1814 255 1826 259 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 550 moveto
+1148 540 lineto
+1144.5 550 lineto
+closepath stroke
+grestore
+% Conv_oracle
+gsave
+0.502 1.000 0.820 nodecolor
+383 522 48.1758 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+383 522 48.1758 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+383 517 moveto 71 -0.5 (Conv_oracle) alignedtext
+grestore
+% Names
+gsave
+0.502 1.000 0.820 nodecolor
+288 18 32.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+288 18 32.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+288 13 moveto 38 -0.5 (Names) alignedtext
+grestore
+% Conv_oracle->Names
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 339 515 moveto
+238 497 0 449 0 378 curveto
+0 378 0 378 0 162 curveto
+0 53 166 26 246 20 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 246.398 23.4778 moveto
+256 19 lineto
+245.701 16.5125 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1825 262 moveto
-1836 262 lineto
-1827 256 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1825 262 moveto
-1836 262 lineto
-1827 256 lineto
-closepath
-stroke
-end grestore
-
-%	Typeops
-gsave 10 dict begin
-552 110 36 18 ellipse_path
-stroke
-gsave 10 dict begin
-528 105 moveto
-(Typeops)
-[6.96 6.96 6.96 6.24 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	Typeops -> Inductive
-newpath 589 110 moveto
-600 110 612 110 624 110 curveto
+0.000 0.000 0.000 edgecolor
+newpath 246.398 23.4778 moveto
+256 19 lineto
+245.701 16.5125 lineto
+closepath stroke
+grestore
+% Cooking
+gsave
+0.502 1.000 0.820 nodecolor
+960 1026 37.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+960 1026 37.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+960 1021 moveto 48 -0.5 (Cooking) alignedtext
+grestore
+% Typeops
+gsave
+0.502 1.000 0.820 nodecolor
+960 954 37.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+960 954 37.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+960 949 moveto 48 -0.5 (Typeops) alignedtext
+grestore
+% Cooking->Typeops
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 960 1008 moveto
+960 1000 960 991 960 982 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 963.5 982 moveto
+960 972 lineto
+956.5 982 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 624 114 moveto
-634 110 lineto
-624 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 624 114 moveto
-634 110 lineto
-624 107 lineto
-closepath
-stroke
-end grestore
-
-%	Entries
-gsave 10 dict begin
-801 56 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-780 51 moveto
-(Entries)
-[8.4 6.96 3.84 4.8 3.84 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Typeops -> Entries
-newpath 581 99 moveto
-595 93 614 87 630 83 curveto
-673 73 723 66 758 61 curveto
+0.000 0.000 0.000 edgecolor
+newpath 963.5 982 moveto
+960 972 lineto
+956.5 982 lineto
+closepath stroke
+grestore
+% Entries
+gsave
+0.502 1.000 0.820 nodecolor
+1391 882 33.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1391 882 33.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1391 877 moveto 40 -0.5 (Entries) alignedtext
+grestore
+% Typeops->Entries
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 995 948 moveto
+1074 935 1265 903 1349 889 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1349.88 892.393 moveto
+1359 887 lineto
+1348.51 885.529 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 758 64 moveto
-768 60 lineto
-758 58 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 758 64 moveto
-768 60 lineto
-758 58 lineto
-closepath
-stroke
-end grestore
-
-%	Sign
-gsave 10 dict begin
-1427 100 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-1414 95 moveto
-(Sign)
-[7.68 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Entries -> Sign
-newpath 834 61 moveto
-882 68 974 79 1053 79 curveto
-1053 79 1053 79 1174 79 curveto
-1251 79 1342 89 1390 95 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1349.88 892.393 moveto
+1359 887 lineto
+1348.51 885.529 lineto
+closepath stroke
+grestore
+% Inductive
+gsave
+0.502 1.000 0.820 nodecolor
+837 882 39.1754 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+837 882 39.1754 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+837 877 moveto 53 -0.5 (Inductive) alignedtext
+grestore
+% Typeops->Inductive
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 936 940 moveto
+918 929 891 914 871 901 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 872.441 897.797 moveto
+862 896 lineto
+869.042 903.916 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1390 98 moveto
-1400 96 lineto
-1390 92 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1390 98 moveto
-1400 96 lineto
-1390 92 lineto
-closepath
-stroke
-end grestore
-
-%	Reduction
-gsave 10 dict begin
-926 208 42 18 ellipse_path
-stroke
-gsave 10 dict begin
-897 203 moveto
-(Reduction)
-[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Type_errors -> Reduction
-newpath 829 125 moveto
-836 129 842 133 848 137 curveto
-868 151 887 170 902 184 curveto
+0.000 0.000 0.000 edgecolor
+newpath 872.441 897.797 moveto
+862 896 lineto
+869.042 903.916 lineto
+closepath stroke
+grestore
+% Csymtable
+gsave
+0.502 1.000 0.820 nodecolor
+1148 666 42.1756 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1148 666 42.1756 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1148 661 moveto 59 -0.5 (Csymtable) alignedtext
+grestore
+% Csymtable->Environ
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1148 648 moveto
+1148 640 1148 631 1148 622 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 622 moveto
+1148 612 lineto
+1144.5 622 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 900 187 moveto
-910 191 lineto
-905 182 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 900 187 moveto
-910 191 lineto
-905 182 lineto
-closepath
-stroke
-end grestore
-
-%	Reduction -> Conv_oracle
-newpath 948 224 moveto
-968 239 999 261 1023 278 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 622 moveto
+1148 612 lineto
+1144.5 622 lineto
+closepath stroke
+grestore
+% Vm
+gsave
+0.502 1.000 0.820 nodecolor
+731 594 27 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+731 594 27 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+731 589 moveto 21 -0.5 (Vm) alignedtext
+grestore
+% Csymtable->Vm
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1109 659 moveto
+1029 645 845 614 767 600 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 767.492 596.529 moveto
+757 598 lineto
+766.119 603.393 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1021 281 moveto
-1031 284 lineto
-1025 275 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1021 281 moveto
-1031 284 lineto
-1025 275 lineto
-closepath
-stroke
-end grestore
-
-%	Closure
-gsave 10 dict begin
-1053 208 35 18 ellipse_path
-stroke
-gsave 10 dict begin
-1031 203 moveto
-(Closure)
-[9.36 3.84 6.96 5.52 6.96 4.56 6.24]
-xshow
-end grestore
-end grestore
-
-%	Reduction -> Closure
-newpath 968 208 moveto
-981 208 994 208 1008 208 curveto
+0.000 0.000 0.000 edgecolor
+newpath 767.492 596.529 moveto
+757 598 lineto
+766.119 603.393 lineto
+closepath stroke
+grestore
+% Vm->Cemitcodes
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 727 576 moveto
+716 527 684 392 669 334 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 672.393 333.119 moveto
+667 324 lineto
+665.529 334.492 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1008 212 moveto
-1018 208 lineto
-1008 205 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1008 212 moveto
-1018 208 lineto
-1008 205 lineto
-closepath
-stroke
-end grestore
-
-%	Term_typing
-gsave 10 dict begin
-313 110 49 18 ellipse_path
-stroke
-gsave 10 dict begin
-277 105 moveto
-(Term_typing)
-[7.2 6.24 4.8 10.8 6.96 3.84 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Term_typing -> Cbytegen
-newpath 347 123 moveto
-363 128 381 134 398 137 curveto
-524 161 675 165 752 165 curveto
+0.000 0.000 0.000 edgecolor
+newpath 672.393 333.119 moveto
+667 324 lineto
+665.529 334.492 lineto
+closepath stroke
+grestore
+% Vm->Conv_oracle
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 705 589 moveto
+648 577 510 549 435 533 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 435.492 529.529 moveto
+425 531 lineto
+434.119 536.393 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 752 169 moveto
-762 165 lineto
-752 162 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 752 169 moveto
-762 165 lineto
-752 162 lineto
-closepath
-stroke
-end grestore
-
-%	Cooking
-gsave 10 dict begin
-436 225 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-411 220 moveto
-(Cooking)
-[9.36 6.96 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Term_typing -> Cooking
-newpath 331 127 moveto
-352 147 387 179 410 202 curveto
+0.000 0.000 0.000 edgecolor
+newpath 435.492 529.529 moveto
+425 531 lineto
+434.119 536.393 lineto
+closepath stroke
+grestore
+% Declarations->Cemitcodes
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1103 371 moveto
+1013 358 811 328 715 314 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 715.492 310.529 moveto
+705 312 lineto
+714.119 317.393 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 408 205 moveto
-418 209 lineto
-413 200 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 408 205 moveto
-418 209 lineto
-413 200 lineto
-closepath
-stroke
-end grestore
-
-%	Indtypes
-gsave 10 dict begin
-436 110 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-411 105 moveto
-(Indtypes)
-[4.56 6.96 6.96 3.84 6.96 6.96 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Term_typing -> Indtypes
-newpath 362 110 moveto
-370 110 379 110 388 110 curveto
+0.000 0.000 0.000 edgecolor
+newpath 715.492 310.529 moveto
+705 312 lineto
+714.119 317.393 lineto
+closepath stroke
+grestore
+% Sign
+gsave
+0.502 1.000 0.820 nodecolor
+1697 306 27 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1697 306 27 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1697 301 moveto 26 -0.5 (Sign) alignedtext
+grestore
+% Declarations->Sign
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1193 372 moveto
+1300 359 1563 324 1660 311 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1660.4 314.478 moveto
+1670 310 lineto
+1659.7 307.512 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 388 114 moveto
-398 110 lineto
-388 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 388 114 moveto
-398 110 lineto
-388 107 lineto
-closepath
-stroke
-end grestore
-
-%	Environ
-gsave 10 dict begin
-1174 181 36 18 ellipse_path
-stroke
-gsave 10 dict begin
-1151 176 moveto
-(Environ)
-[8.4 6.48 6.96 3.84 4.56 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Cbytegen -> Environ
-newpath 841 166 moveto
-911 169 1054 175 1128 179 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1660.4 314.478 moveto
+1670 310 lineto
+1659.7 307.512 lineto
+closepath stroke
+grestore
+% Retroknowledge
+gsave
+0.502 1.000 0.820 nodecolor
+1221 306 59.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1221 306 59.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1221 301 moveto 92 -0.5 (Retroknowledge) alignedtext
+grestore
+% Declarations->Retroknowledge
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1165 361 moveto
+1175 352 1186 341 1197 330 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1199.4 332.546 moveto
+1204 323 lineto
+1194.45 327.596 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1128 183 moveto
-1138 179 lineto
-1128 176 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1128 183 moveto
-1138 179 lineto
-1128 176 lineto
-closepath
-stroke
-end grestore
-
-%	Cooking -> Reduction
-newpath 473 227 moveto
-485 228 498 229 510 229 curveto
-603 231 626 233 718 229 curveto
-773 226 834 220 876 214 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1199.4 332.546 moveto
+1204 323 lineto
+1194.45 327.596 lineto
+closepath stroke
+grestore
+% Sign->Term
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1671 300 moveto
+1576 277 1241 197 1130 170 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1130.49 166.529 moveto
+1120 168 lineto
+1129.12 173.393 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 876 217 moveto
-886 213 lineto
-876 211 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 876 217 moveto
-886 213 lineto
-876 211 lineto
-closepath
-stroke
-end grestore
-
-%	Indtypes -> Typeops
-newpath 474 110 moveto
-484 110 495 110 505 110 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1130.49 166.529 moveto
+1120 168 lineto
+1129.12 173.393 lineto
+closepath stroke
+grestore
+% Retroknowledge->Cbytecodes
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1230 288 moveto
+1234 280 1239 270 1244 261 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1247.2 262.441 moveto
+1249 252 lineto
+1241.08 259.042 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 505 114 moveto
-515 110 lineto
-505 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 505 114 moveto
-515 110 lineto
-505 107 lineto
-closepath
-stroke
-end grestore
-
-%	Term
-gsave 10 dict begin
-1666 173 28 18 ellipse_path
-stroke
-gsave 10 dict begin
-1651 168 moveto
-(Term)
-[7.2 6.24 4.8 10.8]
-xshow
-end grestore
-end grestore
-
-%	Term -> Univ
-newpath 1685 186 moveto
-1699 196 1719 211 1736 222 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1247.2 262.441 moveto
+1249 252 lineto
+1241.08 259.042 lineto
+closepath stroke
+grestore
+% Entries->Sign
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1411 868 moveto
+1442 844 1496 795 1496 738 curveto
+1496 738 1496 738 1496 450 curveto
+1496 370 1604 330 1661 314 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1661.88 317.393 moveto
+1671 312 lineto
+1660.51 310.529 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1734 225 moveto
-1744 228 lineto
-1738 219 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1734 225 moveto
-1744 228 lineto
-1738 219 lineto
-closepath
-stroke
-end grestore
-
-%	Esubst
-gsave 10 dict begin
-1763 173 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-1743 168 moveto
-(Esubst)
-[8.4 5.52 6.96 6.96 5.28 3.84]
-xshow
-end grestore
-end grestore
-
-%	Term -> Esubst
-newpath 1694 173 moveto
-1702 173 1711 173 1720 173 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1661.88 317.393 moveto
+1671 312 lineto
+1660.51 310.529 lineto
+closepath stroke
+grestore
+% Indtypes
+gsave
+0.502 1.000 0.820 nodecolor
+539 1026 37.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+539 1026 37.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+539 1021 moveto 48 -0.5 (Indtypes) alignedtext
+grestore
+% Indtypes->Typeops
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 574 1020 moveto
+650 1008 831 977 915 962 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 915.881 965.393 moveto
+925 960 lineto
+914.508 958.529 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1720 177 moveto
-1730 173 lineto
-1720 170 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1720 177 moveto
-1730 173 lineto
-1720 170 lineto
-closepath
-stroke
-end grestore
-
-%	Subtyping
-gsave 10 dict begin
-552 56 42 18 ellipse_path
-stroke
-gsave 10 dict begin
-523 51 moveto
-(Subtyping)
-[7.68 6.96 6.96 3.84 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Subtyping -> Inductive
-newpath 581 69 moveto
-597 77 618 86 636 93 curveto
+0.000 0.000 0.000 edgecolor
+newpath 915.881 965.393 moveto
+925 960 lineto
+914.508 958.529 lineto
+closepath stroke
+grestore
+% Type_errors
+gsave
+0.502 1.000 0.820 nodecolor
+713 810 47.1758 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+713 810 47.1758 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+713 805 moveto 69 -0.5 (Type_errors) alignedtext
+grestore
+% Inductive->Type_errors
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 813 868 moveto
+794 858 769 843 748 830 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 749.441 826.797 moveto
+739 825 lineto
+746.042 832.916 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 634 96 moveto
-645 97 lineto
-637 90 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 634 96 moveto
-645 97 lineto
-637 90 lineto
-closepath
-stroke
-end grestore
-
-%	Modops
-gsave 10 dict begin
-674 18 36 18 ellipse_path
-stroke
-gsave 10 dict begin
-650 13 moveto
-(Modops)
-[12.48 6.96 6.96 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	Subtyping -> Modops
-newpath 586 45 moveto
-601 41 618 35 633 31 curveto
+0.000 0.000 0.000 edgecolor
+newpath 749.441 826.797 moveto
+739 825 lineto
+746.042 832.916 lineto
+closepath stroke
+grestore
+% Reduction
+gsave
+0.502 1.000 0.820 nodecolor
+713 738 41.1755 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+713 738 41.1755 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+713 733 moveto 57 -0.5 (Reduction) alignedtext
+grestore
+% Type_errors->Reduction
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 713 792 moveto
+713 784 713 775 713 766 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 716.5 766 moveto
+713 756 lineto
+709.5 766 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 634 34 moveto
-643 28 lineto
-632 28 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 634 34 moveto
-643 28 lineto
-632 28 lineto
-closepath
-stroke
-end grestore
-
-%	Modops -> Entries
-newpath 705 27 moveto
-722 32 743 39 761 44 curveto
+0.000 0.000 0.000 edgecolor
+newpath 716.5 766 moveto
+713 756 lineto
+709.5 766 lineto
+closepath stroke
+grestore
+% Modops
+gsave
+0.502 1.000 0.820 nodecolor
+1404 954 35.1752 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1404 954 35.1752 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1404 949 moveto 45 -0.5 (Modops) alignedtext
+grestore
+% Modops->Environ
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1439 951 moveto
+1511 943 1670 914 1670 810 curveto
+1670 810 1670 810 1670 738 curveto
+1670 639 1322 606 1194 597 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1194.3 593.512 moveto
+1184 596 lineto
+1193.6 600.478 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 760 47 moveto
-771 47 lineto
-762 41 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 760 47 moveto
-771 47 lineto
-762 41 lineto
-closepath
-stroke
-end grestore
-
-%	Modops -> Cbytegen
-newpath 686 35 moveto
-695 48 707 67 718 83 curveto
-735 107 733 118 754 137 curveto
-757 140 761 143 765 145 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1194.3 593.512 moveto
+1184 596 lineto
+1193.6 600.478 lineto
+closepath stroke
+grestore
+% Modops->Entries
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1401 936 moveto
+1400 928 1398 919 1396 910 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1399.39 909.119 moveto
+1394 900 lineto
+1392.53 910.492 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 763 148 moveto
-773 151 lineto
-767 142 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 763 148 moveto
-773 151 lineto
-767 142 lineto
-closepath
-stroke
-end grestore
-
-%	Sign -> Term
-newpath 1454 99 moveto
-1489 98 1553 100 1602 119 curveto
-1626 129 1637 135 1649 148 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1399.39 909.119 moveto
+1394 900 lineto
+1392.53 910.492 lineto
+closepath stroke
+grestore
+% Mod_typing
+gsave
+0.502 1.000 0.820 nodecolor
+1157 1170 47.1758 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1157 1170 47.1758 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1157 1165 moveto 69 -0.5 (Mod_typing) alignedtext
+grestore
+% Subtyping
+gsave
+0.502 1.000 0.820 nodecolor
+1404 1026 42.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1404 1026 42.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1404 1021 moveto 58 -0.5 (Subtyping) alignedtext
+grestore
+% Mod_typing->Subtyping
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1183 1155 moveto
+1227 1129 1320 1075 1370 1046 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1371.96 1048.92 moveto
+1379 1041 lineto
+1368.56 1042.8 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1647 151 moveto
-1656 156 lineto
-1652 146 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1647 151 moveto
-1656 156 lineto
-1652 146 lineto
-closepath
-stroke
-end grestore
-
-%	Safe_typing
-gsave 10 dict begin
-47 85 46 18 ellipse_path
-stroke
-gsave 10 dict begin
-13 80 moveto
-(Safe_typing)
-[7.68 6.24 4.08 6.24 6.96 3.84 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Mod_typing
-gsave 10 dict begin
-179 85 48 18 ellipse_path
-stroke
-gsave 10 dict begin
-143 80 moveto
-(Mod_typing)
-[12.48 6.96 6.96 6.96 3.84 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Safe_typing -> Mod_typing
-newpath 94 85 moveto
-103 85 111 85 120 85 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1371.96 1048.92 moveto
+1379 1041 lineto
+1368.56 1042.8 lineto
+closepath stroke
+grestore
+% Term_typing
+gsave
+0.502 1.000 0.820 nodecolor
+960 1098 50.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+960 1098 50.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+960 1093 moveto 74 -0.5 (Term_typing) alignedtext
+grestore
+% Mod_typing->Term_typing
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1123 1157 moveto
+1090 1145 1040 1127 1005 1114 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1005.58 1110.52 moveto
+995 1111 lineto
+1003.57 1117.23 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 120 89 moveto
-130 85 lineto
-120 82 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 120 89 moveto
-130 85 lineto
-120 82 lineto
-closepath
-stroke
-end grestore
-
-%	Mod_typing -> Term_typing
-newpath 223 93 moveto
-235 95 248 98 260 100 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1005.58 1110.52 moveto
+995 1111 lineto
+1003.57 1117.23 lineto
+closepath stroke
+grestore
+% Subtyping->Typeops
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1365 1020 moveto
+1282 1007 1092 975 1005 962 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1005.49 958.529 moveto
+995 960 lineto
+1004.12 965.393 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 260 103 moveto
-270 102 lineto
-261 97 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 260 103 moveto
-270 102 lineto
-261 97 lineto
-closepath
-stroke
-end grestore
-
-%	Mod_typing -> Subtyping
-newpath 227 81 moveto
-297 75 428 65 500 60 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1005.49 958.529 moveto
+995 960 lineto
+1004.12 965.393 lineto
+closepath stroke
+grestore
+% Subtyping->Modops
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1404 1008 moveto
+1404 1000 1404 991 1404 982 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1407.5 982 moveto
+1404 972 lineto
+1400.5 982 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 500 63 moveto
-510 59 lineto
-500 57 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 500 63 moveto
-510 59 lineto
-500 57 lineto
-closepath
-stroke
-end grestore
-
-%	Closure -> Environ
-newpath 1085 201 moveto
-1099 198 1116 194 1131 190 curveto
+0.000 0.000 0.000 edgecolor
+newpath 1407.5 982 moveto
+1404 972 lineto
+1400.5 982 lineto
+closepath stroke
+grestore
+% Term_typing->Cooking
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 960 1080 moveto
+960 1072 960 1063 960 1054 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 963.5 1054 moveto
+960 1044 lineto
+956.5 1054 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1132 193 moveto
-1141 188 lineto
-1131 187 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1132 193 moveto
-1141 188 lineto
-1131 187 lineto
-closepath
-stroke
-end grestore
-
-%	Mod_subst -> Term
-newpath 1594 155 moveto
-1606 158 1618 161 1630 164 curveto
+0.000 0.000 0.000 edgecolor
+newpath 963.5 1054 moveto
+960 1044 lineto
+956.5 1054 lineto
+closepath stroke
+grestore
+% Term_typing->Indtypes
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 915 1090 moveto
+833 1077 665 1048 584 1034 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 584.492 1030.53 moveto
+574 1032 lineto
+583.119 1037.39 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1630 167 moveto
-1640 166 lineto
-1631 161 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1630 167 moveto
-1640 166 lineto
-1631 161 lineto
-closepath
-stroke
-end grestore
-
-%	Declarations
-gsave 10 dict begin
-1295 181 49 18 ellipse_path
-stroke
-gsave 10 dict begin
-1259 176 moveto
-(Declarations)
-[10.08 6.24 6.24 3.84 6.24 4.56 6.24 3.84 3.84 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	Environ -> Declarations
-newpath 1210 181 moveto
-1218 181 1227 181 1236 181 curveto
+0.000 0.000 0.000 edgecolor
+newpath 584.492 1030.53 moveto
+574 1032 lineto
+583.119 1037.39 lineto
+closepath stroke
+grestore
+% Reduction->Closure
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 713 720 moveto
+713 712 713 703 713 694 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 716.5 694 moveto
+713 684 lineto
+709.5 694 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1236 185 moveto
-1246 181 lineto
-1236 178 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1236 185 moveto
-1246 181 lineto
-1236 178 lineto
-closepath
-stroke
-end grestore
-
-%	Declarations -> Cemitcodes
-newpath 1341 188 moveto
-1351 189 1363 191 1373 192 curveto
+0.000 0.000 0.000 edgecolor
+newpath 716.5 694 moveto
+713 684 lineto
+709.5 694 lineto
+closepath stroke
+grestore
+% Reduction->Conv_oracle
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 690 723 moveto
+633 686 482 587 415 544 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 417.1 541.2 moveto
+407 538 lineto
+412.9 546.8 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1373 195 moveto
-1383 194 lineto
-1374 189 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1373 195 moveto
-1383 194 lineto
-1374 189 lineto
-closepath
-stroke
-end grestore
-
-%	Declarations -> Sign
-newpath 1320 165 moveto
-1343 152 1375 132 1398 118 curveto
+0.000 0.000 0.000 edgecolor
+newpath 417.1 541.2 moveto
+407 538 lineto
+412.9 546.8 lineto
+closepath stroke
+grestore
+% Safe_typing
+gsave
+0.502 1.000 0.820 nodecolor
+1157 1242 47.1777 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1157 1242 47.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1157 1237 moveto 68 -0.5 (Safe_typing) alignedtext
+grestore
+% Safe_typing->Mod_typing
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1157 1224 moveto
+1157 1216 1157 1207 1157 1198 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1160.5 1198 moveto
+1157 1188 lineto
+1153.5 1198 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1401 120 moveto
-1407 112 lineto
-1397 115 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1401 120 moveto
-1407 112 lineto
-1397 115 lineto
-closepath
+0.000 0.000 0.000 edgecolor
+newpath 1160.5 1198 moveto
+1157 1188 lineto
+1153.5 1198 lineto
+closepath stroke
+grestore
+% Univ->Names
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 555 84 moveto
+504 71 388 42 327 27 curveto
 stroke
-end grestore
-
-%	Cbytecodes -> Term
-newpath 1595 190 moveto
-1607 188 1619 185 1630 182 curveto
+0.000 0.000 0.000 edgecolor
+newpath 327.492 23.5292 moveto
+317 25 lineto
+326.119 30.3933 lineto
+closepath fill
+0.393658 setlinewidth
+solid
+0.000 0.000 0.000 edgecolor
+newpath 327.492 23.5292 moveto
+317 25 lineto
+326.119 30.3933 lineto
+closepath stroke
+grestore
+% Vconv
+gsave
+0.502 1.000 0.820 nodecolor
+1152 810 31.1748 18 ellipse_path fill
+0.393658 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+1152 810 31.1748 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+1152 805 moveto 37 -0.5 (Vconv) alignedtext
+grestore
+% Vconv->Csymtable
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1151 792 moveto
+1150 767 1149 723 1148 694 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 694 moveto
+1148 684 lineto
+1144.5 694 lineto
+closepath fill
+0.393658 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1631 185 moveto
-1640 179 lineto
-1629 179 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1631 185 moveto
-1640 179 lineto
-1629 179 lineto
-closepath
+0.000 0.000 0.000 edgecolor
+newpath 1151.5 694 moveto
+1148 684 lineto
+1144.5 694 lineto
+closepath stroke
+grestore
+% Vconv->Reduction
+gsave
+0.393658 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1122 805 moveto
+1047 792 852 760 761 746 curveto
 stroke
-end grestore
+0.000 0.000 0.000 edgecolor
+newpath 761.492 742.529 moveto
+751 744 lineto
+760.119 749.393 lineto
+closepath fill
+0.393658 setlinewidth
+solid
+0.000 0.000 0.000 edgecolor
+newpath 761.492 742.529 moveto
+751 744 lineto
+760.119 749.393 lineto
+closepath stroke
+grestore
 endpage
 showpage
 grestore
@@ -1449,6 +1425,7 @@ grestore
 %%EndPage: 1
 %%Trailer
 %%Pages: 1
+%%BoundingBox: 36 36 535 756
 end
 restore
 %%EOF
diff --git a/dev/ocamlweb-doc/library.dep.ps b/dev/ocamlweb-doc/library.dep.ps
index 1c68240e..c9bb351e 100644
--- a/dev/ocamlweb-doc/library.dep.ps
+++ b/dev/ocamlweb-doc/library.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
-%%For: (herbelin) Hugo Herbelin
+%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
+%%For: (notin) Jean-Marc Notin,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 35 35 577 207
+%%BoundingBox: (atend)
 %%EndComments
 save
 %%BeginProlog
@@ -16,57 +16,7 @@ mark
  EncodingVector 0
 
 ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
-  dup 306 /AE
-  dup 301 /Aacute
-  dup 302 /Acircumflex
-  dup 304 /Adieresis
-  dup 300 /Agrave
-  dup 305 /Aring
-  dup 303 /Atilde
-  dup 307 /Ccedilla
-  dup 311 /Eacute
-  dup 312 /Ecircumflex
-  dup 313 /Edieresis
-  dup 310 /Egrave
-  dup 315 /Iacute
-  dup 316 /Icircumflex
-  dup 317 /Idieresis
-  dup 314 /Igrave
-  dup 334 /Udieresis
-  dup 335 /Yacute
-  dup 376 /thorn
-  dup 337 /germandbls
-  dup 341 /aacute
-  dup 342 /acircumflex
-  dup 344 /adieresis
-  dup 346 /ae
-  dup 340 /agrave
-  dup 345 /aring
-  dup 347 /ccedilla
-  dup 351 /eacute
-  dup 352 /ecircumflex
-  dup 353 /edieresis
-  dup 350 /egrave
-  dup 355 /iacute
-  dup 356 /icircumflex
-  dup 357 /idieresis
-  dup 354 /igrave
-  dup 360 /dcroat
-  dup 361 /ntilde
-  dup 363 /oacute
-  dup 364 /ocircumflex
-  dup 366 /odieresis
-  dup 362 /ograve
-  dup 365 /otilde
-  dup 370 /oslash
-  dup 372 /uacute
-  dup 373 /ucircumflex
-  dup 374 /udieresis
-  dup 371 /ugrave
-  dup 375 /yacute
-  dup 377 /ydieresis  
+EncodingVector 45 /hyphen put
 
 % Set up ISO Latin 1 character encoding
 /starnetISO {
@@ -98,8 +48,8 @@ cleartomark
 
 /InvScaleFactor 1.0 def
 /set_scale {
-	dup 1 exch div /InvScaleFactor exch def
-	dup scale
+       dup 1 exch div /InvScaleFactor exch def
+       scale
 } bind def
 
 % styles
@@ -229,601 +179,587 @@ def
 } if
 
 %%EndSetup
+setupLatin1
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 207
-%%PageOrientation: Portrait
+%%PageBoundingBox: 36 36 576 752
+%%PageOrientation: Landscape
 gsave
-35 35 542 172 boxprim clip newpath
-36 36 translate
+36 36 576 752 boxprim clip newpath
 0 0 1 beginpage
-0.6750 set_scale
-0 0 translate 0 rotate
-0.000 0.000 0.000 graphcolor
+0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate
+0.000 0.000 1.000 graphcolor
+newpath -4 -4 moveto
+-4 544 lineto
+723 544 lineto
+723 -4 lineto
+closepath fill
+0.985401 setlinewidth
+0.000 0.000 1.000 graphcolor
+newpath -4 -4 moveto
+-4 544 lineto
+723 544 lineto
+723 -4 lineto
+closepath stroke
+% Declare
+gsave
+0.502 1.000 0.820 nodecolor
+488 436 34.1751 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+488 436 34.1751 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
 14.00 /Times-Roman set_font
-
-%	States
-gsave 10 dict begin
-30 18 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-13 13 moveto
-(States)
-[7.44 4.08 6.24 3.84 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Library
-gsave 10 dict begin
-132 18 34 18 ellipse_path
-stroke
-gsave 10 dict begin
-110 13 moveto
-(Library)
-[8.4 3.84 6.96 4.56 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-%	States -> Library
-newpath 60 18 moveto
-69 18 78 18 87 18 curveto
+488 431 moveto 43 -0.5 (Declare) alignedtext
+grestore
+% Dischargedhypsmap
+gsave
+0.502 1.000 0.820 nodecolor
+488 353 69.1764 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+488 353 69.1764 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+488 348 moveto 113 -0.5 (Dischargedhypsmap) alignedtext
+grestore
+% Declare->Dischargedhypsmap
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 488 418 moveto
+488 407 488 393 488 381 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 491.5 381 moveto
+488 371 lineto
+484.5 381 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 87 22 moveto
-97 18 lineto
-87 15 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 87 22 moveto
-97 18 lineto
-87 15 lineto
-closepath
-stroke
-end grestore
-
-%	Declaremods
-gsave 10 dict begin
-274 18 50 18 ellipse_path
-stroke
-gsave 10 dict begin
-236 13 moveto
-(Declaremods)
-[10.08 6.24 6.24 3.84 6.24 4.56 6.24 10.8 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	Library -> Declaremods
-newpath 167 18 moveto
-181 18 197 18 213 18 curveto
+0.000 0.000 0.000 edgecolor
+newpath 491.5 381 moveto
+488 371 lineto
+484.5 381 lineto
+closepath stroke
+grestore
+% Impargs
+gsave
+0.502 1.000 0.820 nodecolor
+201 353 36.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+201 353 36.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+201 348 moveto 46 -0.5 (Impargs) alignedtext
+grestore
+% Declare->Impargs
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 458 427 moveto
+407 412 301 382 242 365 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 242.584 361.521 moveto
+232 362 lineto
+240.573 368.226 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 213 22 moveto
-223 18 lineto
-213 15 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 213 22 moveto
-223 18 lineto
-213 15 lineto
-closepath
-stroke
-end grestore
-
-%	Nametab
-gsave 10 dict begin
-523 134 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-497 129 moveto
-(Nametab)
-[9.6 6.24 10.8 6 4.08 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-%	Libnames
-gsave 10 dict begin
-642 134 41 18 ellipse_path
-stroke
-gsave 10 dict begin
-613 129 moveto
-(Libnames)
-[8.4 3.84 6.96 6.96 6.24 10.8 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Nametab -> Libnames
-newpath 562 134 moveto
-571 134 580 134 590 134 curveto
+0.000 0.000 0.000 edgecolor
+newpath 242.584 361.521 moveto
+232 362 lineto
+240.573 368.226 lineto
+closepath stroke
+grestore
+% Decl_kinds
+gsave
+0.502 1.000 0.820 nodecolor
+661 353 44.1757 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+661 353 44.1757 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+661 348 moveto 63 -0.5 (Decl_kinds) alignedtext
+grestore
+% Declare->Decl_kinds
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 514 424 moveto
+543 410 590 388 624 372 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 625.958 374.916 moveto
+633 367 lineto
+622.559 368.797 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 590 138 moveto
-600 134 lineto
-590 131 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 590 138 moveto
-600 134 lineto
-590 131 lineto
-closepath
-stroke
-end grestore
-
-%	Summary
-gsave 10 dict begin
-642 65 40 18 ellipse_path
-stroke
-gsave 10 dict begin
-614 60 moveto
-(Summary)
-[7.68 6.96 10.8 10.8 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-%	Nametab -> Summary
-newpath 547 120 moveto
-565 110 589 96 608 84 curveto
+0.000 0.000 0.000 edgecolor
+newpath 625.958 374.916 moveto
+633 367 lineto
+622.559 368.797 lineto
+closepath stroke
+grestore
+% Lib
+gsave
+0.502 1.000 0.820 nodecolor
+219 270 27 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+219 270 27 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+219 265 moveto 20 -0.5 (Lib) alignedtext
+grestore
+% Dischargedhypsmap->Lib
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 443 339 moveto
+390 323 302 296 254 281 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 254.584 277.521 moveto
+244 278 lineto
+252.573 284.226 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 610 87 moveto
-617 79 lineto
-607 81 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 610 87 moveto
-617 79 lineto
-607 81 lineto
-closepath
-stroke
-end grestore
-
-%	Nameops
-gsave 10 dict begin
-760 134 40 18 ellipse_path
-stroke
-gsave 10 dict begin
-733 129 moveto
-(Nameops)
-[9.6 6.24 10.8 6.24 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	Libnames -> Nameops
-newpath 684 134 moveto
-693 134 701 134 710 134 curveto
+0.000 0.000 0.000 edgecolor
+newpath 254.584 277.521 moveto
+244 278 lineto
+252.573 284.226 lineto
+closepath stroke
+grestore
+% Global
+gsave
+0.502 1.000 0.820 nodecolor
+82 270 32.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+82 270 32.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+82 265 moveto 38 -0.5 (Global) alignedtext
+grestore
+% Impargs->Global
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 180 338 moveto
+161 325 132 305 110 290 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 112.1 287.2 moveto
+102 284 lineto
+107.9 292.8 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 710 138 moveto
-720 134 lineto
-710 131 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 710 138 moveto
-720 134 lineto
-710 131 lineto
-closepath
-stroke
-end grestore
-
-%	Lib
-gsave 10 dict begin
-413 153 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-402 148 moveto
-(Lib)
-[8.4 3.84 6.96]
-xshow
-end grestore
-end grestore
-
-%	Declaremods -> Lib
-newpath 315 29 moveto
-325 33 336 38 344 45 curveto
-359 58 383 99 399 127 curveto
+0.000 0.000 0.000 edgecolor
+newpath 112.1 287.2 moveto
+102 284 lineto
+107.9 292.8 lineto
+closepath stroke
+grestore
+% Impargs->Lib
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 205 335 moveto
+207 324 210 310 213 298 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 216.471 298.492 moveto
+215 288 lineto
+209.607 297.119 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 396 129 moveto
-404 136 lineto
-402 126 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 396 129 moveto
-404 136 lineto
-402 126 lineto
-closepath
-stroke
-end grestore
-
-%	Global
-gsave 10 dict begin
-413 65 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-393 60 moveto
-(Global)
-[10.08 3.84 6.96 6.96 6.24 3.84]
-xshow
-end grestore
-end grestore
-
-%	Declaremods -> Global
-newpath 311 30 moveto
-331 37 355 45 375 52 curveto
+0.000 0.000 0.000 edgecolor
+newpath 216.471 298.492 moveto
+215 288 lineto
+209.607 297.119 lineto
+closepath stroke
+grestore
+% Declaremods
+gsave
+0.502 1.000 0.820 nodecolor
+65 353 49.1759 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+65 353 49.1759 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+65 348 moveto 73 -0.5 (Declaremods) alignedtext
+grestore
+% Declaremods->Global
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 69 335 moveto
+71 324 74 310 76 298 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 79.4708 298.492 moveto
+78 288 lineto
+72.6067 297.119 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 374 55 moveto
-385 55 lineto
-376 49 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 374 55 moveto
-385 55 lineto
-376 49 lineto
-closepath
-stroke
-end grestore
-
-%	Libobject
-gsave 10 dict begin
-523 188 40 18 ellipse_path
-stroke
-gsave 10 dict begin
-495 183 moveto
-(Libobject)
-[8.4 3.84 6.96 6.96 6.96 3.84 6.24 6.24 3.84]
-xshow
-end grestore
-end grestore
-
-%	Libobject -> Libnames
-newpath 552 175 moveto
-567 168 587 159 604 151 curveto
+0.000 0.000 0.000 edgecolor
+newpath 79.4708 298.492 moveto
+78 288 lineto
+72.6067 297.119 lineto
+closepath stroke
+grestore
+% Declaremods->Lib
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 93 338 moveto
+120 324 161 301 189 286 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 190.958 288.916 moveto
+198 281 lineto
+187.559 282.797 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 605 154 moveto
-613 147 lineto
-602 148 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 605 154 moveto
-613 147 lineto
-602 148 lineto
-closepath
-stroke
-end grestore
-
-%	Lib -> Nametab
-newpath 439 148 moveto
-450 146 464 144 476 142 curveto
+0.000 0.000 0.000 edgecolor
+newpath 190.958 288.916 moveto
+198 281 lineto
+187.559 282.797 lineto
+closepath stroke
+grestore
+% Summary
+gsave
+0.502 1.000 0.820 nodecolor
+69 103 40.1755 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+69 103 40.1755 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+69 98 moveto 55 -0.5 (Summary) alignedtext
+grestore
+% Global->Summary
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 81 252 moveto
+78 223 74 166 71 131 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 74.4778 130.602 moveto
+70 121 lineto
+67.5125 131.299 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 477 145 moveto
-486 140 lineto
-476 139 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 477 145 moveto
-486 140 lineto
-476 139 lineto
-closepath
-stroke
-end grestore
-
-%	Lib -> Libobject
-newpath 437 161 moveto
-450 165 466 170 480 174 curveto
+0.000 0.000 0.000 edgecolor
+newpath 74.4778 130.602 moveto
+70 121 lineto
+67.5125 131.299 lineto
+closepath stroke
+grestore
+% Libnames
+gsave
+0.502 1.000 0.820 nodecolor
+203 103 40.1755 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+203 103 40.1755 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+203 98 moveto 55 -0.5 (Libnames) alignedtext
+grestore
+% Global->Libnames
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 94 253 moveto
+115 224 159 164 184 129 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 186.8 131.1 moveto
+190 121 lineto
+181.2 126.9 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 479 177 moveto
-490 177 lineto
-481 171 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 479 177 moveto
-490 177 lineto
-481 171 lineto
-closepath
-stroke
-end grestore
-
-%	Impargs
-gsave 10 dict begin
-274 126 36 18 ellipse_path
-stroke
-gsave 10 dict begin
-251 121 moveto
-(Impargs)
-[4.56 10.56 6.96 6.24 4.32 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	Impargs -> Lib
-newpath 308 133 moveto
-329 137 355 142 377 146 curveto
+0.000 0.000 0.000 edgecolor
+newpath 186.8 131.1 moveto
+190 121 lineto
+181.2 126.9 lineto
+closepath stroke
+grestore
+% Nametab
+gsave
+0.502 1.000 0.820 nodecolor
+203 186 38.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+203 186 38.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+203 181 moveto 50 -0.5 (Nametab) alignedtext
+grestore
+% Lib->Nametab
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 216 252 moveto
+214 241 211 226 209 214 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 212.393 213.119 moveto
+207 204 lineto
+205.529 214.492 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 377 149 moveto
-387 148 lineto
-378 143 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 377 149 moveto
-387 148 lineto
-378 143 lineto
-closepath
-stroke
-end grestore
-
-%	Impargs -> Global
-newpath 304 116 moveto
-316 111 331 105 344 99 curveto
-357 94 369 88 381 82 curveto
+0.000 0.000 0.000 edgecolor
+newpath 212.393 213.119 moveto
+207 204 lineto
+205.529 214.492 lineto
+closepath stroke
+grestore
+% Libobject
+gsave
+0.502 1.000 0.820 nodecolor
+329 186 40.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+329 186 40.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+329 181 moveto 54 -0.5 (Libobject) alignedtext
+grestore
+% Lib->Libobject
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 237 256 moveto
+254 243 280 223 300 208 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 302.1 210.8 moveto
+308 202 lineto
+297.9 205.2 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 382 85 moveto
-390 78 lineto
-379 79 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 382 85 moveto
-390 78 lineto
-379 79 lineto
-closepath
-stroke
-end grestore
-
-%	Global -> Libnames
-newpath 443 73 moveto
-473 81 522 94 564 107 curveto
-576 111 589 115 600 119 curveto
+0.000 0.000 0.000 edgecolor
+newpath 302.1 210.8 moveto
+308 202 lineto
+297.9 205.2 lineto
+closepath stroke
+grestore
+% Nameops
+gsave
+0.502 1.000 0.820 nodecolor
+203 20 39.1777 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+203 20 39.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+203 15 moveto 52 -0.5 (Nameops) alignedtext
+grestore
+% Libnames->Nameops
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 203 85 moveto
+203 74 203 60 203 48 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 206.5 48 moveto
+203 38 lineto
+199.5 48 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 599 122 moveto
-610 122 lineto
-601 116 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 599 122 moveto
-610 122 lineto
-601 116 lineto
-closepath
-stroke
-end grestore
-
-%	Global -> Summary
-newpath 446 65 moveto
-484 65 547 65 591 65 curveto
+0.000 0.000 0.000 edgecolor
+newpath 206.5 48 moveto
+203 38 lineto
+199.5 48 lineto
+closepath stroke
+grestore
+% Goptions
+gsave
+0.502 1.000 0.820 nodecolor
+322 353 38.1754 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+322 353 38.1754 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+322 348 moveto 51 -0.5 (Goptions) alignedtext
+grestore
+% Goptions->Lib
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 303 337 moveto
+287 324 263 305 245 291 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 246.831 287.951 moveto
+237 284 lineto
+242.221 293.219 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 591 69 moveto
-601 65 lineto
-591 62 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 591 69 moveto
-601 65 lineto
-591 62 lineto
-closepath
-stroke
-end grestore
-
-%	Goptions
-gsave 10 dict begin
-274 180 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-248 175 moveto
-(Goptions)
-[10.08 6.96 6.96 3.84 3.84 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	Goptions -> Lib
-newpath 310 173 moveto
-331 169 356 164 377 160 curveto
+0.000 0.000 0.000 edgecolor
+newpath 246.831 287.951 moveto
+237 284 lineto
+242.221 293.219 lineto
+closepath stroke
+grestore
+% Nametab->Summary
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 180 172 moveto
+158 159 125 138 101 123 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 102.441 119.797 moveto
+92 118 lineto
+99.0418 125.916 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 378 163 moveto
-387 158 lineto
-377 157 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 378 163 moveto
-387 158 lineto
-377 157 lineto
-closepath
-stroke
-end grestore
-
-%	Dischargedhypsmap
-gsave 10 dict begin
-274 234 70 18 ellipse_path
-stroke
-gsave 10 dict begin
-217 229 moveto
-(Dischargedhypsmap)
-[10.08 3.84 5.52 6 6.96 6.24 4.32 6.72 6.24 6.96 6.48 6.96 6.96 5.52 10.8 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-%	Dischargedhypsmap -> Lib
-newpath 317 220 moveto
-326 216 336 212 344 207 curveto
-360 197 376 185 389 175 curveto
+0.000 0.000 0.000 edgecolor
+newpath 102.441 119.797 moveto
+92 118 lineto
+99.0418 125.916 lineto
+closepath stroke
+grestore
+% Nametab->Libnames
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 203 168 moveto
+203 157 203 143 203 131 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 206.5 131 moveto
+203 121 lineto
+199.5 131 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 392 177 moveto
-397 168 lineto
-387 172 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 392 177 moveto
-397 168 lineto
-387 172 lineto
-closepath
-stroke
-end grestore
-
-%	Declare
-gsave 10 dict begin
-132 126 35 18 ellipse_path
-stroke
-gsave 10 dict begin
-109 121 moveto
-(Declare)
-[10.08 6.24 6.24 3.84 6.24 4.56 6.24]
-xshow
-end grestore
-end grestore
-
-%	Declare -> Impargs
-newpath 168 126 moveto
-186 126 208 126 228 126 curveto
+0.000 0.000 0.000 edgecolor
+newpath 206.5 131 moveto
+203 121 lineto
+199.5 131 lineto
+closepath stroke
+grestore
+% Libobject->Libnames
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 306 171 moveto
+286 158 256 138 235 124 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 236.262 120.635 moveto
+226 118 lineto
+232.379 126.459 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 228 130 moveto
-238 126 lineto
-228 123 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 228 130 moveto
-238 126 lineto
-228 123 lineto
-closepath
-stroke
-end grestore
-
-%	Declare -> Dischargedhypsmap
-newpath 144 143 moveto
-157 161 179 189 204 207 curveto
-209 210 215 213 221 216 curveto
+0.000 0.000 0.000 edgecolor
+newpath 236.262 120.635 moveto
+226 118 lineto
+232.379 126.459 lineto
+closepath stroke
+grestore
+% Library
+gsave
+0.502 1.000 0.820 nodecolor
+65 436 34.1751 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+65 436 34.1751 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+65 431 moveto 43 -0.5 (Library) alignedtext
+grestore
+% Library->Declaremods
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 65 418 moveto
+65 407 65 393 65 381 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 68.5001 381 moveto
+65 371 lineto
+61.5001 381 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 219 219 moveto
-230 220 lineto
-222 213 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 219 219 moveto
-230 220 lineto
-222 213 lineto
-closepath
-stroke
-end grestore
-
-%	Decl_kinds
-gsave 10 dict begin
-274 72 45 18 ellipse_path
-stroke
-gsave 10 dict begin
-241 67 moveto
-(Decl_kinds)
-[10.08 6.24 6.24 3.84 6.96 6.96 3.84 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	Declare -> Decl_kinds
-newpath 161 115 moveto
-181 107 209 97 232 88 curveto
+0.000 0.000 0.000 edgecolor
+newpath 68.5001 381 moveto
+65 371 lineto
+61.5001 381 lineto
+closepath stroke
+grestore
+% States
+gsave
+0.502 1.000 0.820 nodecolor
+65 519 29.1747 18 ellipse_path fill
+0.985401 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+65 519 29.1747 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+65 514 moveto 33 -0.5 (States) alignedtext
+grestore
+% States->Library
+gsave
+0.985401 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 65 501 moveto
+65 490 65 476 65 464 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 68.5001 464 moveto
+65 454 lineto
+61.5001 464 lineto
+closepath fill
+0.985401 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 233 91 moveto
-241 84 lineto
-230 85 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 233 91 moveto
-241 84 lineto
-230 85 lineto
-closepath
-stroke
-end grestore
+0.000 0.000 0.000 edgecolor
+newpath 68.5001 464 moveto
+65 454 lineto
+61.5001 464 lineto
+closepath stroke
+grestore
 endpage
 showpage
 grestore
@@ -831,6 +767,7 @@ grestore
 %%EndPage: 1
 %%Trailer
 %%Pages: 1
+%%BoundingBox: 36 36 576 752
 end
 restore
 %%EOF
diff --git a/dev/ocamlweb-doc/proofs.dep.ps b/dev/ocamlweb-doc/proofs.dep.ps
index 0e78f422..4dd045ce 100644
--- a/dev/ocamlweb-doc/proofs.dep.ps
+++ b/dev/ocamlweb-doc/proofs.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
-%%For: (herbelin) Hugo Herbelin
+%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
+%%For: (notin) Jean-Marc Notin,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 35 35 577 136
+%%BoundingBox: (atend)
 %%EndComments
 save
 %%BeginProlog
@@ -16,57 +16,7 @@ mark
  EncodingVector 0
 
 ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
-  dup 306 /AE
-  dup 301 /Aacute
-  dup 302 /Acircumflex
-  dup 304 /Adieresis
-  dup 300 /Agrave
-  dup 305 /Aring
-  dup 303 /Atilde
-  dup 307 /Ccedilla
-  dup 311 /Eacute
-  dup 312 /Ecircumflex
-  dup 313 /Edieresis
-  dup 310 /Egrave
-  dup 315 /Iacute
-  dup 316 /Icircumflex
-  dup 317 /Idieresis
-  dup 314 /Igrave
-  dup 334 /Udieresis
-  dup 335 /Yacute
-  dup 376 /thorn
-  dup 337 /germandbls
-  dup 341 /aacute
-  dup 342 /acircumflex
-  dup 344 /adieresis
-  dup 346 /ae
-  dup 340 /agrave
-  dup 345 /aring
-  dup 347 /ccedilla
-  dup 351 /eacute
-  dup 352 /ecircumflex
-  dup 353 /edieresis
-  dup 350 /egrave
-  dup 355 /iacute
-  dup 356 /icircumflex
-  dup 357 /idieresis
-  dup 354 /igrave
-  dup 360 /dcroat
-  dup 361 /ntilde
-  dup 363 /oacute
-  dup 364 /ocircumflex
-  dup 366 /odieresis
-  dup 362 /ograve
-  dup 365 /otilde
-  dup 370 /oslash
-  dup 372 /uacute
-  dup 373 /ucircumflex
-  dup 374 /udieresis
-  dup 371 /ugrave
-  dup 375 /yacute
-  dup 377 /ydieresis  
+EncodingVector 45 /hyphen put
 
 % Set up ISO Latin 1 character encoding
 /starnetISO {
@@ -98,8 +48,8 @@ cleartomark
 
 /InvScaleFactor 1.0 def
 /set_scale {
-	dup 1 exch div /InvScaleFactor exch def
-	dup scale
+       dup 1 exch div /InvScaleFactor exch def
+       scale
 } bind def
 
 % styles
@@ -229,403 +179,463 @@ def
 } if
 
 %%EndSetup
+setupLatin1
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 136
-%%PageOrientation: Portrait
+%%PageBoundingBox: 36 36 576 753
+%%PageOrientation: Landscape
 gsave
-35 35 542 101 boxprim clip newpath
-36 36 translate
+36 36 576 753 boxprim clip newpath
 0 0 1 beginpage
-0.6923 set_scale
-0 0 translate 0 rotate
-0.000 0.000 0.000 graphcolor
+0.870968 0.870968 set_scale 90 rotate 45.3333 -657.333 translate
+0.000 0.000 1.000 graphcolor
+newpath -4 -4 moveto
+-4 616 lineto
+819 616 lineto
+819 -4 lineto
+closepath fill
+0.870968 setlinewidth
+0.000 0.000 1.000 graphcolor
+newpath -4 -4 moveto
+-4 616 lineto
+819 616 lineto
+819 -4 lineto
+closepath stroke
+% Clenvtac
+gsave
+0.502 1.000 0.820 nodecolor
+451 522 37.1753 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+451 522 37.1753 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
 14.00 /Times-Roman set_font
-
-%	Tactic_debug
-gsave 10 dict begin
-163 72 51 18 ellipse_path
-stroke
-gsave 10 dict begin
-125 67 moveto
-(Tactic_debug)
-[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 6.24 6.96 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	Refiner
-gsave 10 dict begin
-287 72 34 18 ellipse_path
-stroke
-gsave 10 dict begin
-266 67 moveto
-(Refiner)
-[9.12 6.24 4.8 3.84 6.96 6.24 4.56]
-xshow
-end grestore
-end grestore
-
-%	Tactic_debug -> Refiner
-newpath 214 72 moveto
-223 72 233 72 243 72 curveto
+451 517 moveto 49 -0.5 (Clenvtac) alignedtext
+grestore
+% Evar_refiner
+gsave
+0.502 1.000 0.820 nodecolor
+439 450 49.1777 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+439 450 49.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+439 445 moveto 72 -0.5 (Evar_refiner) alignedtext
+grestore
+% Clenvtac->Evar_refiner
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 448 504 moveto
+447 496 445 487 444 478 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 447.393 477.119 moveto
+442 468 lineto
+440.529 478.492 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 243 76 moveto
-253 72 lineto
-243 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 243 76 moveto
-253 72 lineto
-243 69 lineto
-closepath
-stroke
-end grestore
-
-%	Logic
-gsave 10 dict begin
-390 72 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-373 67 moveto
-(Logic)
-[8.4 6.96 6.96 3.84 6.24]
-xshow
-end grestore
-end grestore
-
-%	Refiner -> Logic
-newpath 321 72 moveto
-330 72 340 72 350 72 curveto
+0.000 0.000 0.000 edgecolor
+newpath 447.393 477.119 moveto
+442 468 lineto
+440.529 478.492 lineto
+closepath stroke
+grestore
+% Tacmach
+gsave
+0.502 1.000 0.820 nodecolor
+711 450 38.1754 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+711 450 38.1754 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+711 445 moveto 51 -0.5 (Tacmach) alignedtext
+grestore
+% Clenvtac->Tacmach
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 483 513 moveto
+530 500 616 476 668 462 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 669.427 465.226 moveto
+678 459 lineto
+667.416 458.521 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 350 76 moveto
-360 72 lineto
-350 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 350 76 moveto
-360 72 lineto
-350 69 lineto
-closepath
-stroke
-end grestore
-
-%	Tacmach
-gsave 10 dict begin
-163 126 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-137 121 moveto
-(Tacmach)
-[7.44 6.24 6.24 10.8 6.24 6 6.96]
-xshow
-end grestore
-end grestore
-
-%	Tacmach -> Refiner
-newpath 191 114 moveto
-209 106 232 96 251 88 curveto
+0.000 0.000 0.000 edgecolor
+newpath 669.427 465.226 moveto
+678 459 lineto
+667.416 458.521 lineto
+closepath stroke
+grestore
+% Refiner
+gsave
+0.502 1.000 0.820 nodecolor
+439 378 34.1777 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+439 378 34.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+439 373 moveto 42 -0.5 (Refiner) alignedtext
+grestore
+% Evar_refiner->Refiner
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 439 432 moveto
+439 424 439 415 439 406 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 442.5 406 moveto
+439 396 lineto
+435.5 406 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 253 91 moveto
-261 84 lineto
-250 84 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 253 91 moveto
-261 84 lineto
-250 84 lineto
-closepath
-stroke
-end grestore
-
-%	Redexpr
-gsave 10 dict begin
-287 126 36 18 ellipse_path
-stroke
-gsave 10 dict begin
-263 121 moveto
-(Redexpr)
-[9.12 6.24 6.96 5.76 6.96 6.96 4.56]
-xshow
-end grestore
-end grestore
-
-%	Tacmach -> Redexpr
-newpath 202 126 moveto
-214 126 227 126 240 126 curveto
+0.000 0.000 0.000 edgecolor
+newpath 442.5 406 moveto
+439 396 lineto
+435.5 406 lineto
+closepath stroke
+grestore
+% Tacmach->Refiner
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 678 441 moveto
+628 428 533 403 480 389 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 480.584 385.521 moveto
+470 386 lineto
+478.573 392.226 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 240 130 moveto
-250 126 lineto
-240 123 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 240 130 moveto
-250 126 lineto
-240 123 lineto
-closepath
-stroke
-end grestore
-
-%	Proof_trees
-gsave 10 dict begin
-502 72 45 18 ellipse_path
-stroke
-gsave 10 dict begin
-469 67 moveto
-(Proof_trees)
-[7.68 4.56 6.96 6.96 4.56 6.96 3.84 4.56 6.24 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-%	Logic -> Proof_trees
-newpath 420 72 moveto
-428 72 437 72 446 72 curveto
+0.000 0.000 0.000 edgecolor
+newpath 480.584 385.521 moveto
+470 386 lineto
+478.573 392.226 lineto
+closepath stroke
+grestore
+% Redexpr
+gsave
+0.502 1.000 0.820 nodecolor
+711 378 36.1752 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+711 378 36.1752 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+711 373 moveto 47 -0.5 (Redexpr) alignedtext
+grestore
+% Tacmach->Redexpr
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 711 432 moveto
+711 424 711 415 711 406 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 714.5 406 moveto
+711 396 lineto
+707.5 406 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 446 76 moveto
-456 72 lineto
-446 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 446 76 moveto
-456 72 lineto
-446 69 lineto
-closepath
-stroke
-end grestore
-
-%	Proof_type
-gsave 10 dict begin
-628 72 44 18 ellipse_path
-stroke
-gsave 10 dict begin
-597 67 moveto
-(Proof_type)
-[7.68 4.56 6.96 6.96 4.56 6.96 3.84 6.96 6.96 6.24]
-xshow
-end grestore
-end grestore
-
-%	Tacexpr
-gsave 10 dict begin
-744 72 35 18 ellipse_path
-stroke
-gsave 10 dict begin
-721 67 moveto
-(Tacexpr)
-[7.44 6.24 6.24 5.76 6.96 6.96 4.56]
-xshow
-end grestore
-end grestore
-
-%	Proof_type -> Tacexpr
-newpath 672 72 moveto
-680 72 689 72 698 72 curveto
+0.000 0.000 0.000 edgecolor
+newpath 714.5 406 moveto
+711 396 lineto
+707.5 406 lineto
+closepath stroke
+grestore
+% Decl_mode
+gsave
+0.502 1.000 0.820 nodecolor
+698 594 45.1777 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+698 594 45.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+698 589 moveto 64 -0.5 (Decl_mode) alignedtext
+grestore
+% Pfedit
+gsave
+0.502 1.000 0.820 nodecolor
+698 522 30.1777 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+698 522 30.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+698 517 moveto 34 -0.5 (Pfedit) alignedtext
+grestore
+% Decl_mode->Pfedit
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 698 576 moveto
+698 568 698 559 698 550 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 701.5 550 moveto
+698 540 lineto
+694.5 550 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 698 76 moveto
-708 72 lineto
-698 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 698 76 moveto
-708 72 lineto
-698 69 lineto
-closepath
-stroke
-end grestore
-
-%	Proof_trees -> Proof_type
-newpath 548 72 moveto
-557 72 565 72 574 72 curveto
+0.000 0.000 0.000 edgecolor
+newpath 701.5 550 moveto
+698 540 lineto
+694.5 550 lineto
+closepath stroke
+grestore
+% Pfedit->Evar_refiner
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 671 514 moveto
+628 503 543 479 488 464 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 488.584 460.521 moveto
+478 461 lineto
+486.573 467.226 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 574 76 moveto
-584 72 lineto
-574 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 574 76 moveto
-584 72 lineto
-574 69 lineto
-closepath
-stroke
-end grestore
-
-%	Pfedit
-gsave 10 dict begin
-38 112 29 18 ellipse_path
-stroke
-gsave 10 dict begin
-21 107 moveto
-(Pfedit)
-[7.68 4.08 6.24 6.96 3.84 3.84]
-xshow
-end grestore
-end grestore
-
-%	Pfedit -> Tacmach
-newpath 67 115 moveto
-81 117 99 118 115 120 curveto
+0.000 0.000 0.000 edgecolor
+newpath 488.584 460.521 moveto
+478 461 lineto
+486.573 467.226 lineto
+closepath stroke
+grestore
+% Pfedit->Tacmach
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 701 504 moveto
+702 496 704 487 706 478 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 709.471 478.492 moveto
+708 468 lineto
+702.607 477.119 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 115 123 moveto
-125 122 lineto
-116 117 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 115 123 moveto
-125 122 lineto
-116 117 lineto
-closepath
-stroke
-end grestore
-
-%	Evar_refiner
-gsave 10 dict begin
-163 18 49 18 ellipse_path
-stroke
-gsave 10 dict begin
-127 13 moveto
-(Evar_refiner)
-[8.4 6.72 6.24 4.56 6.96 4.56 6.24 4.8 3.84 6.96 6.24 4.56]
-xshow
-end grestore
-end grestore
-
-%	Pfedit -> Evar_refiner
-newpath 53 96 moveto
-67 82 90 60 112 45 curveto
-116 42 120 40 124 37 curveto
+0.000 0.000 0.000 edgecolor
+newpath 709.471 478.492 moveto
+708 468 lineto
+702.607 477.119 lineto
+closepath stroke
+grestore
+% Logic
+gsave
+0.502 1.000 0.820 nodecolor
+439 306 29.1747 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+439 306 29.1747 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+439 301 moveto 33 -0.5 (Logic) alignedtext
+grestore
+% Refiner->Logic
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 439 360 moveto
+439 352 439 343 439 334 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 442.5 334 moveto
+439 324 lineto
+435.5 334 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 126 40 moveto
-133 32 lineto
-123 34 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 126 40 moveto
-133 32 lineto
-123 34 lineto
-closepath
-stroke
-end grestore
-
-%	Evar_refiner -> Refiner
-newpath 195 32 moveto
-212 40 233 49 251 57 curveto
+0.000 0.000 0.000 edgecolor
+newpath 442.5 334 moveto
+439 324 lineto
+435.5 334 lineto
+closepath stroke
+grestore
+% Proof_trees
+gsave
+0.502 1.000 0.820 nodecolor
+439 234 45.1757 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+439 234 45.1757 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+439 229 moveto 65 -0.5 (Proof_trees) alignedtext
+grestore
+% Logic->Proof_trees
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 439 288 moveto
+439 280 439 271 439 262 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 442.5 262 moveto
+439 252 lineto
+435.5 262 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 249 60 moveto
-260 61 lineto
-252 54 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 249 60 moveto
-260 61 lineto
-252 54 lineto
-closepath
-stroke
-end grestore
-
-%	Clenvtac
-gsave 10 dict begin
-38 45 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-13 40 moveto
-(Clenvtac)
-[9.36 3.84 6.24 6.48 6.96 4.08 6.24 6.24]
-xshow
-end grestore
-end grestore
-
-%	Clenvtac -> Tacmach
-newpath 58 61 moveto
-73 72 93 87 112 99 curveto
-117 102 123 105 128 108 curveto
+0.000 0.000 0.000 edgecolor
+newpath 442.5 262 moveto
+439 252 lineto
+435.5 262 lineto
+closepath stroke
+grestore
+% Proof_type
+gsave
+0.502 1.000 0.820 nodecolor
+439 162 44.1757 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+439 162 44.1757 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+439 157 moveto 63 -0.5 (Proof_type) alignedtext
+grestore
+% Proof_trees->Proof_type
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 439 216 moveto
+439 208 439 199 439 190 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 442.5 190 moveto
+439 180 lineto
+435.5 190 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 127 111 moveto
-137 113 lineto
-130 105 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 127 111 moveto
-137 113 lineto
-130 105 lineto
-closepath
+0.000 0.000 0.000 edgecolor
+newpath 442.5 190 moveto
+439 180 lineto
+435.5 190 lineto
+closepath stroke
+grestore
+% Decl_expr
+gsave
+0.502 1.000 0.820 nodecolor
+439 90 42.1777 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+439 90 42.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+439 85 moveto 58 -0.5 (Decl_expr) alignedtext
+grestore
+% Proof_type->Decl_expr
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 439 144 moveto
+439 136 439 127 439 118 curveto
 stroke
-end grestore
-
-%	Clenvtac -> Evar_refiner
-newpath 73 37 moveto
-85 35 98 32 110 29 curveto
+0.000 0.000 0.000 edgecolor
+newpath 442.5 118 moveto
+439 108 lineto
+435.5 118 lineto
+closepath fill
+0.870968 setlinewidth
+solid
+0.000 0.000 0.000 edgecolor
+newpath 442.5 118 moveto
+439 108 lineto
+435.5 118 lineto
+closepath stroke
+grestore
+% Tacexpr
+gsave
+0.502 1.000 0.820 nodecolor
+439 18 36.1777 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+439 18 36.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+439 13 moveto 46 -0.5 (Tacexpr) alignedtext
+grestore
+% Decl_expr->Tacexpr
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 439 72 moveto
+439 64 439 55 439 46 curveto
 stroke
-gsave 10 dict begin
+0.000 0.000 0.000 edgecolor
+newpath 442.5 46 moveto
+439 36 lineto
+435.5 46 lineto
+closepath fill
+0.870968 setlinewidth
 solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 111 32 moveto
-120 27 lineto
-110 26 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 111 32 moveto
-120 27 lineto
-110 26 lineto
-closepath
+0.000 0.000 0.000 edgecolor
+newpath 442.5 46 moveto
+439 36 lineto
+435.5 46 lineto
+closepath stroke
+grestore
+% Tactic_debug
+gsave
+0.502 1.000 0.820 nodecolor
+133 450 51.1777 18 ellipse_path fill
+0.870968 setlinewidth
+filled
+0.502 1.000 0.820 nodecolor
+133 450 51.1777 18 ellipse_path stroke
+0.000 0.000 0.000 nodecolor
+14.00 /Times-Roman set_font
+133 445 moveto 76 -0.5 (Tactic_debug) alignedtext
+grestore
+% Tactic_debug->Refiner
+gsave
+0.870968 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 176 440 moveto
+234 426 339 401 398 387 curveto
 stroke
-end grestore
+0.000 0.000 0.000 edgecolor
+newpath 398.881 390.393 moveto
+408 385 lineto
+397.508 383.529 lineto
+closepath fill
+0.870968 setlinewidth
+solid
+0.000 0.000 0.000 edgecolor
+newpath 398.881 390.393 moveto
+408 385 lineto
+397.508 383.529 lineto
+closepath stroke
+grestore
 endpage
 showpage
 grestore
@@ -633,6 +643,7 @@ grestore
 %%EndPage: 1
 %%Trailer
 %%Pages: 1
+%%BoundingBox: 36 36 576 753
 end
 restore
 %%EOF
diff --git a/dev/set_raw_db b/dev/set_raw_db
new file mode 100644
index 00000000..5caff7e5
--- /dev/null
+++ b/dev/set_raw_db
@@ -0,0 +1 @@
+install_printer Top_printers.ppconstrdb
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e1ee29e4..afae141b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -32,6 +32,10 @@ open Genarg
 
 let _ = Constrextern.print_evar_arguments := true
 let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false
+let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
+
+(* std_ppcmds *)
+let pppp x = pp x
 
 (* name printers *)
 let ppid id = pp (pr_id id)
@@ -44,20 +48,26 @@ let ppcon con = pp(pr_con con)
 let ppkn kn = pp(pr_kn kn)
 let ppsp sp = pp(pr_sp sp)
 let ppqualid qid = pp(pr_qualid qid)
+let ppclindex cl = pp(Classops.pr_cl_index cl)
 
 (* term printers *)
-let ppconstr x = pp(Termops.print_constr x)
+let rawdebug = ref false
+let ppconstr x = pp (Termops.print_constr x)
+let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
 let ppterm = ppconstr
 let ppsconstr x = ppconstr (Declarations.force x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let pprawconstr = (fun x -> pp(pr_lrawconstr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
 let pptype = (fun x -> pp(pr_ltype x))
+
 let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
 let ppbigint n = pp (Bigint.pr_bigint n);;
 
-let ppidset l = pp (prlist_with_sep spc pr_id (Idset.elements l))
+let prset pr l = str "[" ++ prlist_with_sep spc pr l ++ str "]"
+let ppintset l = pp (prset int (Intset.elements l))
+let ppidset l = pp (prset pr_id (Idset.elements l))
 
 let pP s = pp (hov 0 s)
 
@@ -81,7 +91,14 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 
 let ppj j = pp (genppj pr_ljudge j)
 
+let prsubst s = pp (Mod_subst.debug_pr_subst s)
+
+let pp_idpred s = pp (pr_idpred s)
+let pp_cpred s = pp (pr_cpred s)
+let pp_transparent_state s = pp (pr_transparent_state s)
+
 (* proof printers *)
+let ppmetas metas = pp(pr_metaset metas)
 let ppevm evd = pp(pr_evar_map evd)
 let ppevd evd = pp(pr_evar_defs evd)
 let ppclenv clenv = pp(pr_clenv clenv)
@@ -103,6 +120,8 @@ let ppuni u = pp(pr_uni u)
 
 let ppuniverses u = pp (str"[" ++ pr_universes u ++ str"]")
 
+let ppconstraints c = pp (pr_constraints c)
+
 let ppenv e = pp
   (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
    str "[" ++ pr_rel_context e (rel_context e) ++ str "]")
@@ -240,8 +259,7 @@ let print_pure_constr csr =
       print_string "end"; 
       close_box()
   | Fix ((t,i),(lna,tl,bl)) ->
-      print_string "Fix"
-(* "("; print_int i; print_string ")"; 
+      print_string "Fix("; print_int i; print_string ")"; 
       print_cut();
       open_vbox 0;
       let rec print_fix () =
@@ -253,7 +271,7 @@ let print_pure_constr csr =
 	  box_display bl.(k); close_box ();
 	  print_cut()
         done
-      in print_string"{"; print_fix(); print_string"}" *)
+      in print_string"{"; print_fix(); print_string"}" 
   | CoFix(i,(lna,tl,bl)) ->
       print_string "CoFix("; print_int i; print_string ")"; 
       print_cut();
@@ -404,3 +422,48 @@ let _ =
          (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr),
           ConstrArgType),
          Some "c")]]
+
+(* Setting printer of unbound global reference *)
+open Names
+open Nameops
+open Libnames
+
+let encode_path loc prefix mpdir suffix id =
+  let dir = match mpdir with
+    | None -> []
+    | Some (mp,dir) -> 
+	(repr_dirpath (dirpath_of_string (string_of_mp mp))@
+	repr_dirpath dir) in
+  Qualid (loc, make_qualid 
+    (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
+
+let raw_string_of_ref loc = function
+  | ConstRef cst -> 
+      let (mp,dir,id) = repr_con cst in
+      encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)
+  | IndRef (kn,i) ->
+      let (mp,dir,id) = repr_kn kn in
+      encode_path loc "IND" (Some (mp,dir)) [id_of_label id] 
+	(id_of_string ("_"^string_of_int i))
+  | ConstructRef ((kn,i),j) -> 
+      let (mp,dir,id) = repr_kn kn in
+      encode_path loc "CSTR" (Some (mp,dir))
+	[id_of_label id;id_of_string ("_"^string_of_int i)] 
+	(id_of_string ("_"^string_of_int j))
+  | VarRef id -> 
+      encode_path loc "SECVAR" None [] id
+
+let short_string_of_ref loc = function
+  | VarRef id -> Ident (loc,id)
+  | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst)))
+  | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_kn kn)))
+  | IndRef (kn,i) ->
+      encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))]
+        (id_of_string ("_"^string_of_int i))
+  | ConstructRef ((kn,i),j) -> 
+      encode_path loc "CSTR" None 
+        [id_of_label (pi3 (repr_kn kn));id_of_string ("_"^string_of_int i)]
+        (id_of_string ("_"^string_of_int j))
+
+let _ = Constrextern.set_debug_global_reference_printer
+  (if !rawdebug then raw_string_of_ref else short_string_of_ref)
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 97973df2..de68ce1e 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -748,7 +748,7 @@ Conflicts exists between integers and constrs.
 \nlsep \TERM{cc}
 %% contrib/field
 \nlsep \TERM{field}~\STAR{\tacconstr}
-%% contrib/first-order
+%% contrib/firstorder
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
author	Samuel Mimram <smimram@debian.org>	2008-07-25 15:12:53 +0200
committer	Samuel Mimram <smimram@debian.org>	2008-07-25 15:12:53 +0200
commit	a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
tree	dabcac548e299fee1da464c93b3dba98484f45b1 /dev
parent	2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)