Imported Upstream version 8.0pl1upstream/8.0pl1

22 files changed, 2139 insertions, 0 deletions

diff --git a/dev/Makefile.common b/dev/Makefile.common
new file mode 100644
index 00000000..1ff5cf79
--- /dev/null
+++ b/dev/Makefile.common
@@ -0,0 +1,52 @@
+# this Makefile contains goals common for directory and main devel makefiles
+
+ifndef TOPDIR
+TOPDIR=..
+endif
+
+ifndef BASEDIR
+BASEDIR=
+endif
+
+# the following entries are used to make synchronize two source trees
+# (on big computer and on a laptop for example)
+
+OTHER_FILE=$(TOPDIR)/dev/other
+OTHER=$(shell cat $(OTHER_FILE))
+
+# this is a directory of useful temporary things
+WORKDIR=tmp
+
+ifneq (,$(findstring n,$(MAKEFLAGS)))
+NFLAG=-n
+else
+NFLAG=
+endif
+
+check_other:
+	+@(if [ "$(OTHER)" = "" ] ; then \
+	  echo You must put the ssh path to the other Coq source in $(OTHER_FILE) ; \
+	  echo For example: chrzaszc@ruta:coq/V7 ; \
+	  exit 1; \
+	fi)
+
+get:	check_other
+	+rsync -Cauvz $(NFLAG) $(OTHER)/ $(TOPDIR)/
+	+@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \
+	  rsync -auvz $(NFLAG) $(OTHER)/tmp/ $(TOPDIR)/tmp/ ; \
+	fi)
+
+put:	check_other
+	+rsync -Cauvz $(NFLAG) $(TOPDIR)/ $(OTHER)/
+	+@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \
+	  rsync -auvz $(NFLAG) $(TOPDIR)/tmp/ $(OTHER)/tmp/ ; \
+	fi)
+
+sync:	get put
+
+
+conflicts:
+	cvs status | grep File | grep conflicts | less
+
+confl:	conflicts
+
diff --git a/dev/Makefile.devel b/dev/Makefile.devel
new file mode 100644
index 00000000..f3abb62d
--- /dev/null
+++ b/dev/Makefile.devel
@@ -0,0 +1,74 @@
+# to be linked to makefile (lowercase - takes precedence over Makefile)
+# in main directory
+# make devel in main directory should do this for you.
+
+TOPDIR=.
+BASEDIR=
+
+SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
+
+default:	usage noargument
+
+usage::
+	@echo Usage: make \<target\>
+	@echo Targets are:
+
+usage::
+	@echo "  setup-devel	-- set the devel makefile"
+setup-devel:
+	@ln -sfv dev/Makefile.devel makefile
+	@(for i in $(SOURCEDIRS); do \
+	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/Makefile.dir Makefile) \
+	done)
+
+
+usage::
+	@echo "  clean-devel	-- clear all devel files"
+clean-devel:
+	echo rm -f makefile .depend.devel
+	echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile)
+
+
+usage::
+	@echo "  coqtop	-- make until the bytecode executable, make the link"
+coqtop:	bin/coqtop.byte
+	ln -sf bin/coqtop.byte coqtop
+
+
+usage::
+	@echo "  quick		-- make bytecode executable and states"
+quick: 
+	$(MAKE) states BEST=byte
+
+include Makefile
+
+include $(TOPDIR)/dev/Makefile.common
+
+# this file is better described in dev/Makefile.dir
+include .depend.devel
+
+#if dev/Makefile.local exists, it is included
+ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),)
+include $(TOPDIR)/dev/Makefile.local
+endif
+
+
+usage::
+	@echo "  total		-- runs coqtop with all theories required"
+total:
+	ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th))))
+
+
+usage::
+	@echo "  run		-- makes and runs bytecode coqtop using ledit and the history file"
+	@echo "		   if you want to pass arguments to coqtop, use make run ARG=<args>"
+run:	$(TOPDIR)/coqtop
+	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS)
+
+
+usage::
+	@echo "  vars		-- echos commands to set COQTOP and COQBIN variables"
+vars:
+	@(cd $(TOPDIR); \
+	echo export COQTOP=`pwd`/ ; \
+	echo export COQBIN=`pwd`/bin/ )
\ No newline at end of file
diff --git a/dev/Makefile.dir b/dev/Makefile.dir
new file mode 100644
index 00000000..54f7bfe9
--- /dev/null
+++ b/dev/Makefile.dir
@@ -0,0 +1,131 @@
+# make a link to this file if you are working hard in one directory of Coq
+#   ln -s ../dev/Makefile.dir Makefile
+# if you are working in a sub/dir/ make a link to dev/Makefile.subdir instead
+# this Makefile provides many useful facilities to develop Coq
+# it is not completely compatible with .ml4 files unfortunately
+
+ifndef TOPDIR
+TOPDIR=..
+endif
+
+# this complicated thing should work for subsubdirs as well
+BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||"))
+
+noargs:	dir
+
+test-dir:
+	@echo TOPDIR=$(TOPDIR)
+	@echo BASEDIR=$(BASEDIR)
+
+include $(TOPDIR)/dev/Makefile.common
+
+# make this directory
+dir:
+	$(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR))
+
+# make all cmo's in this directory. Useful in case the main Makefile is not
+# up-to-date
+all:	
+	@( ( for i in *.ml; do \
+	       echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \
+	     done; \
+	     for i in *.ml4; do \
+	       echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \
+	     done ) \
+	  | xargs $(MAKE) -C $(TOPDIR) )
+
+# lists all files that should be compiled in this directory
+list:
+	@(for i in *.mli; do \
+	   ls -l `basename $$i .mli`.cmi; \
+	done)
+	@(for i in *.ml; do \
+	   ls -l `basename $$i .ml`.cmo; \
+	done)
+	@(for i in *.ml4; do \
+	   ls -l `basename $$i .ml4`.cmo; \
+	done)
+
+
+clean::  
+	rm -f *.cmi *.cmo *.cmx *.o
+
+
+# if grammar.cmo files cannot be compiled and main .depend cannot be
+# rebuilt, this is quite useful
+depend:
+	(cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel)
+
+
+# displays the dependency graph of the current directory (vertically,
+# unlike in doc/)
+graph:
+	(ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) &
+
+
+# the pretty entry draws a dependency graph marking red those nodes
+# which do not have their .cmo files 
+
+.INTERMEDIATE: depend.dot depend.2.dot
+.PHONY: depend.ps
+
+depend.dot:
+	ocamldep *.ml *.mli | ocamldot > $@
+
+depend.2.dot:	depend.dot
+	(i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@
+	(for ml in *.ml; do \
+	   base=`basename $$ml .ml`; \
+	   fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \
+	   rest=`echo $$base | cut -c2-`; \
+	   name=`echo $$fst $$rest | tr -d " "`; \
+	   cmo=$$base.cmo; \
+	   if [ ! -e $$cmo ]; then \
+	     echo \"$$name\" [color=red]\; >> $@;\
+	   fi;\
+         done;\
+	 echo } >> $@)
+
+depend.ps:	depend.2.dot
+	dot -Tps $< > $@
+
+clean::
+	rm -f depend.ps
+
+pretty:	depend.ps
+	(gv -spartan $<; rm $<) &
+#	gv -spartan $< &
+
+
+
+# generating file.ml.mli by tricking make to pass -i to ocamlc 
+
+%.ml.mli:	FORCE
+	@(cmo=`basename $@ .ml.mli`.cmo ; \
+	mv -f $$cmo $$cmo.tmp ; \
+	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \
+	echo Generated interface file $@ ; \
+	mv -f $$cmo.tmp $$cmo)
+
+%.annot:	FORCE
+	@(cmo=`basename $@ .annot`.cmo ; \
+	mv -f $$cmo $$cmo.tmp ; \
+	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \
+	echo Generated annotation file $@ ; \
+	mv -f $$cmo.tmp $$cmo)
+
+FORCE:
+
+clean::
+	rm -f *.ml.mli
+
+# this is not perfect but mostly WORKS! It just calls the main makefile
+
+%.cmi:	FORCE
+	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
+
+%.cmo:	FORCE
+	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
+
+coqtop:	
+	$(MAKE) -C $(TOPDIR) bin/coqtop.byte
diff --git a/dev/Makefile.subdir b/dev/Makefile.subdir
new file mode 100644
index 00000000..45358c42
--- /dev/null
+++ b/dev/Makefile.subdir
@@ -0,0 +1,7 @@
+# if you work in a sub/sub-rectory of Coq
+# you should make a link to that makefile 
+#    ln -s ../../dev/Makefile.subdir Makefile
+# in order to have all the facilities of dev/Makefile.dir
+
+TOPDIR=../..
+include $(TOPDIR)/dev/Makefile.dir
diff --git a/dev/README b/dev/README
new file mode 100644
index 00000000..a8811bea
--- /dev/null
+++ b/dev/README
@@ -0,0 +1,21 @@
+This directory contains informations and tools to help developping the
+Coq system
+
+
+TODO
+changements.txt
+header
+lisezmoi.txt			   
+style.txt			   
+
+Debugging and profiling
+=======================
+
+debugging.txt: help for debugging or profiling
+db: to install pretty-printers from ocaml debugger
+base_db: to install raw pretty-printers from ocaml debugger
+ocamldebug-v7: to launch ocaml debugger
+include: to install pretty-printers from ocaml toplevel
+base_include: to install raw pretty-printers from ocaml toplevel
+universes.txt: help to debug universes
+univdot: produces a graph of CIC universes
diff --git a/dev/TODO b/dev/TODO
new file mode 100644
index 00000000..926861c9
--- /dev/null
+++ b/dev/TODO
@@ -0,0 +1,22 @@
+
+ o options de la ligne de commande
+     - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml
+
+ o arguments implicites
+     - les calculer une fois pour toutes à la déclaration (dans Declare)
+       et stocker cette information dans le in_variable, in_constant, etc.
+
+ o Environnements compilés (type Environ.compiled_env)
+     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)
+
+ o Efficacité
+     - utiliser DOPL plutôt que DOPN (sauf pour Case)
+     - batch mode => pas de undo, ni de reset
+     - conversion : déplier la constante la plus récente
+     - un cache pour type_of_const, type_of_inductive, type_of_constructor,
+       lookup_mind_specif
+
+ o Toplevel
+     - parsing de la ligne de commande : utiliser Arg ???
+
+
diff --git a/dev/base_db b/dev/base_db
new file mode 100644
index 00000000..b540aed6
--- /dev/null
+++ b/dev/base_db
@@ -0,0 +1,6 @@
+load_printer "gramlib.cma"
+load_printer "top_printers.cmo"
+install_printer Top_printers.prid
+install_printer Top_printers.prsp
+install_printer Top_printers.print_pure_constr
+
diff --git a/dev/base_include b/dev/base_include
new file mode 100644
index 00000000..17293776
--- /dev/null
+++ b/dev/base_include
@@ -0,0 +1,76 @@
+
+(* File to include to get some Coq facilities under the ocaml toplevel.
+   This file is loaded by include *)
+
+#cd".";;
+#directory "parsing";;
+#directory "interp";;
+#directory "toplevel";;
+#directory "library";;
+#directory "kernel";;
+#directory "pretyping";;
+#directory "lib";;
+#directory "proofs";;
+#directory "tactics";;
+#directory "translate";;
+#use "top_printers.ml";;
+
+#install_printer  (* identifier *) prid;;
+#install_printer  (* label *) prlab;;
+#install_printer prmsid;;
+#install_printer prmbid;;
+#install_printer prdir;;
+#install_printer prmp;;
+#install_printer  (* section_path *)  prsp;;
+#install_printer  (* qualid *)  prqualid;;
+#install_printer  (* kernel_name *) prkn;;
+#install_printer  (* constr *)  print_pure_constr;;
+
+(* parsing of names *)
+
+let qid = Libnames.qualid_of_string;;
+
+(* parsing of terms *)
+
+let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
+let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;;
+let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
+
+(* For compatibility reasons *)
+let parse_ast = parse_com;;
+
+(* build a term of type rawconstr without type-checking or resolution of 
+   implicit syntax *)
+
+let e s = Constrintern.interp_rawconstr Evd.empty (Global.env()) (parse_ast s);;
+
+(* For compatibility *)
+let raw_constr_of_string = e;;
+
+(* build a term of type constr with type-checking and resolution of 
+   implicit syntax *)
+
+let constr_of_string s = 
+  Constrintern.interp_constr Evd.empty (Global.env()) (parse_ast s);;
+
+(* get the body of a constant *)
+
+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;;
+
+(* Get the current goal *)
+
+let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);;
+
+let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());;
+let current_goal () = get_nth_goal 1;;
+
+let pf_e gl s = 
+    Constrintern.interp_constr (project gl) (pf_env gl) (parse_ast s);;
+
+open Toplevel
+let go = loop
+
diff --git a/dev/changements.txt b/dev/changements.txt
new file mode 100644
index 00000000..d1df2a81
--- /dev/null
+++ b/dev/changements.txt
@@ -0,0 +1,455 @@
+CHANGES DUE TO INTRODUCTION OF MODULES
+======================================
+
+1.Kernel
+--------
+
+  The module level has no effect on constr except for the structure of
+section_path. The type of unique names for constructions (what
+section_path served) is now called a kernel name and is defined by
+ 
+type uniq_ident = int * string * dir_path (* int may be enough *)
+type module_path =
+  | MPfile of dir_path    (* reference to physical module, e.g. file *)
+  | MPbound of uniq_ident (* reference to a module parameter in a functor *)
+  | MPself of uniq_ident  (* reference to one of the containing module *)
+  | MPdot of module_path * label
+type label = identifier
+type kernel_name = module_path * dir_path * label
+                   ^^^^^^^^^^^   ^^^^^^^^   ^^^^^
+                        |           |         \
+                        |           |          the base name
+                        |           \
+                       /             the (true) section path
+   example:                          (non empty only inside open sections)
+   L = (* i.e. some file of logical name L *)
+   struct
+     module A = struct Def a = ... end
+   end
+   M = (* i.e. some file of logical name M *)
+   struct
+     Def t = ...
+     N = functor (X : sig module T = struct Def b = ... end end) -> struct
+       module O = struct
+         Def u = ...
+       end
+       Def x := ... <M>.t ... <N>.O.u ... X.T.b ... L.A.a
+ 
+   <M> and <N> are self-references, X is a bound reference and L is a
+reference to a physical module.
+ 
+  Notice that functor application is not part of a path: it must be
+named by a "module M = F(A)" declaration to be used in a kernel
+name.
+ 
+  Notice that Jacek chose a practical approach, making directories not
+modules. Another approach could have been to replace the constructor
+MPfile by a constant constructor MProot representing the root of the
+world.
+ 
+  Other relevant informations are in kernel/entries.ml (type
+module_expr) and kernel/declarations.ml (type module_body and
+module_type_body).                                                              
+
+2. Library
+----------
+
+i) tables 
+[Summaries] - the only change is the special treatment of the
+global environmet.
+
+ii) objects 
+[Libobject] declares persistent objects, given with methods:
+
+   * cache_function specifying how to add the object in the current
+       scope;
+   * load_function, specifying what to do when the module 
+       containing the object is loaded; 
+   * open_function, specifying what to do when the module 
+       containing the object is opened (imported);
+   * classify_function, specyfying what to do with the object,
+       when the current module (containing the object) is ended. 
+   * subst_function
+   * export_function, to signal end_section survival
+
+(Almost) Each of these methods is called with a parameter of type
+object_name = section_path * kernel_name
+where section_path is the full user name of the object (such as
+Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal
+version such as (MPself<Datatypes#1>,[],"Fst") (see above)
+
+
+What happens at the end of an interactive module ?
+==================================================
+(or when a file is stored and reloaded from disk)
+
+All summaries (except Global environment) are reverted to the state
+from before the beginning of the module, and:
+
+a) the objects (again, since last Declaremods.start_module or
+   Library.start_library) are classified using the classify_function.
+   To simplify consider only those who returned Substitute _ or Keep _.
+
+b) If the module is not a functor, the subst_function for each object of
+   the first group is called with the substitution 
+   [MPself "<Datatypes#1>" |-> MPfile "Coq.Init.Datatypes"].
+   Then the load_function is called for substituted objects and the
+   "keep" object. 
+   (If the module is a library the substitution is done at reloading).
+
+c) The objects which returned substitute are stored in the modtab
+   together with the self ident of the module, and functor argument
+   names if the module was a functor.
+
+   They will be used (substituted and loaded) when a command like 
+     Module M := F(N)    or
+     Module Z := N 
+   is evaluated
+
+
+The difference between "substitute" and "keep" objects
+========================================================
+i) The "keep" objects can _only_ reference other objects by section_paths
+and qualids. They do not need the substitution function.
+
+They will work after end_module (or reloading a compiled library),
+because these operations do not change section_path's
+
+They will obviously not work after Module Z:=N.
+ 
+These would typically be grammar rules, pretty printing rules etc.
+
+
+
+ii) The "substitute" objects can _only_ reference objects by
+kernel_names. They must have a valid subst_function. 
+
+They will work after end_module _and_ after Module Z:=N or 
+Module Z:=F(M).
+
+
+
+Other kinds of objects:
+iii) "Dispose" - objects which do not survive end_module
+     As a consequence, objects which reference other objects sometimes
+     by kernel_names and sometimes by section_path must be of this kind...
+
+iv) "Anticipate" - objects which must be treated individually by
+    end_module (typically "REQUIRE" objects)
+
+
+
+Writing subst_thing functions
+=============================
+The subst_thing shoud not copy the thing if it hasn't actually
+changed. There are some cool emacs macros in dev/objects.el 
+to help writing subst functions this way quickly and without errors.
+Also there are *_smartmap functions in Util.
+
+The subst_thing functions are already written for many types,
+including constr (Term.subst_mps), 
+global_reference (Libnames.subst_global),
+rawconstr (Rawterm.subst_raw) etc
+
+They are all (apart from constr, for now) written in the non-copying
+way.
+
+
+Nametab
+=======
+
+Nametab has been made more uniform. For every kind of thing there is
+only one "push" function and one "locate" function. 
+
+
+Lib
+===
+
+library_segment is now a list of object_name * library_item, where
+object_name = section_path * kernel_name (see above)
+
+New items have been added for open modules and module types
+
+
+Declaremods
+==========
+Functions to declare interactive and noninteractive modules and module
+types.
+
+
+Library
+=======
+Uses Declaremods to actually communicate with Global and to register
+objects.
+
+
+MAIN CHANGES FROM COQ V7.3
+==========================
+
+Internal representation of tactics bindings has changed (see type
+Rawterm.substitution).
+
+New parsing model for tactics and vernacular commands
+
+  - Introduction of a dedicated type for tactic expressions
+    (Tacexpr.raw_tactic_expr)
+  - Introduction of a dedicated type for vernac expressions
+    (Vernacexpr.vernac_expr)
+  - Declaration of new vernacular parsing rules by a new camlp4 macro
+    GRAMMAR COMMAND EXTEND ... END  to be used in ML files
+  - Declaration of new tactics parsing/printing rules by a new camlp4 macro
+    TACTIC EXTEND ... END  to be used in ML files
+
+New organisation of THENS:
+tclTHENS tac tacs : tacs is now an array
+tclTHENSFIRSTn tac1 tacs tac2 :
+  apply tac1 then, apply the array tacs on the first n subgoals and
+  tac2 on the remaining subgoals (previously tclTHENST)
+tclTHENSLASTn tac1 tac2 tacs :
+  apply tac1 then, apply tac2 on the first subgoals and apply the array
+  tacs on the last n subgoals
+tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI)
+tclTHENLASTn tac1 tacs  = tclTHENSLASTn tac1 tclIDTAC tacs
+tclTHENFIRST tac1 tac2  = tclTHENFIRSTn tac1 [|tac2|]
+tclTHENLAST tac1 tac2   = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL)
+tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number")
+tclTHENSV same as tclTHENS but with an array
+tclTHENSi : no longer available
+
+Proof_type: subproof field in type proof_tree glued with the ref field
+
+Tacmach: no more echo from functions of module Refiner
+
+Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v.
+Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
+  VERNAC COMMAND EXTEND macros
+File syntax/PPTactic.v moved to parsing/pptactic.ml
+Tactics about False and not now in tactics/contradiction.ml
+Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v)
+File tacinterp.ml moved from proofs to directory tactics
+
+MAIN CHANGES FROM COQ V7.1 TO COQ V7.2
+======================================
+
+The core of Coq (kernel) has meen minimized with the following effects:
+
+kernel/term.ml      split into kernel/term.ml,      pretyping/termops.ml
+kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml
+kernel/names.ml     split into kernel/names.ml,     library/nameops.ml
+kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml
+
+the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors,
+e.g. IsRel is now Rel, IsMutCase is now Case, etc.
+
+
+PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0
+===================================================
+
+Changements d'organisation / modules :
+--------------------------------------
+
+  Std, More_util		-> lib/util.ml
+
+  Names				-> kernel/names.ml et kernel/sign.ml
+    (les parties noms et signatures ont été séparées)
+
+  Avm,Mavm,Fmavm,Mhm  ->  utiliser plutôt Map (et freeze alors gratuit)
+  Mhb                 ->  Bij
+
+  Generic est intégré à Term (et un petit peu à Closure)
+
+Changements dans les types de données :
+---------------------------------------
+  dans Generic: free_rels : constr -> int Listset.t
+                  devient : constr -> Intset.t
+
+  type_judgement ->  typed_type
+  environment    ->  context
+  context        ->  typed_type signature
+
+
+ATTENTION:
+----------
+
+  Il y a maintenant d'autres exceptions que UserError (TypeError,
+  RefinerError, etc.)
+
+  Il ne faut donc plus se contenter (pour rattraper) de faire
+  
+		try . .. with UserError _ -> ...
+
+  mais écrire à la place
+ 
+                try ... with e when Logic.catchable_exception e -> ...
+
+
+Changements dans les fonctions :
+--------------------------------
+
+	Vectops.
+	  it_vect          ->  Array.fold_left
+	  vect_it          ->  Array.fold_right
+	  exists_vect      ->  Util.array_exists
+	  for_all2eq_vect  ->  Util.array_for_all2
+	  tabulate_vect    ->  Array.init
+	  hd_vect          ->  Util.array_hd
+	  tl_vect          ->  Util.array_tl
+	  last_vect        ->  Util.array_last
+	  it_vect_from     ->  array_fold_left_from
+	  vect_it_from     ->  array_fold_right_from
+	  app_tl_vect	   ->  array_app_tl
+	  cons_vect	   ->  array_cons
+	  map_i_vect	   ->  Array.mapi
+	  map2_vect	   ->  array_map2
+	  list_of_tl_vect  ->  array_list_of_tl
+
+        Names
+          sign_it        -> fold_var_context (se fait sur env maintenant)
+	  it_sign        -> fold_var_context_reverse (sur env maintenant)
+
+        Generic
+	  noccur_bet     -> noccur_between
+          substn_many    -> substnl
+
+	Std 
+	  comp           ->  Util.compose
+	  rev_append	 ->  List.rev_append
+
+	Termenv
+	  mind_specif_of_mind  -> Global.lookup_mind_specif
+                ou Environ.lookup_mind_specif si on a un env sous la main
+	  mis_arity      ->  instantiate_arity
+	  mis_lc	 ->  instantiate_lc	
+
+	Ex-Environ	 
+	  mind_of_path      -> Global.lookup_mind
+
+	Printer
+	  gentermpr	->   gen_pr_term
+          term0	        ->   prterm_env	
+          pr_sign       ->   pr_var_context
+	  pr_context_opt -> pr_context_of
+          pr_ne_env      -> pr_ne_context_of
+
+	Typing, Machops
+	  type_of_type     ->  judge_of_type
+	  fcn_proposition  ->  judge_of_prop_contents
+	  safe_fmachine    ->  safe_infer
+
+	Reduction, Clenv
+          whd_betadeltat      -> whd_betaevar
+          whd_betadeltatiota  -> whd_betaiotaevar
+          find_mrectype       -> Inductive.find_mrectype
+          find_minductype     -> Inductive.find_inductive
+          find_mcoinductype   -> Inductive.find_coinductive
+
+        Astterm
+          constr_of_com_casted -> interp_casted_constr
+          constr_of_com_sort   -> interp_type
+          constr_of_com        -> interp_constr
+          rawconstr_of_com     -> interp_rawconstr
+          type_of_com          -> type_judgement_of_rawconstr
+	  judgement_of_com     -> judgement_of_rawconstr
+
+        Termast
+          bdize                -> ast_of_constr
+
+        Tacmach
+          pf_constr_of_com_sort -> pf_interp_type
+          pf_constr_of_com      -> pf_interp_constr
+	  pf_get_hyp            -> pf_get_hyp_typ
+          pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant)
+
+        Pattern
+	  raw_sopattern_of_compattern -> Astterm.interp_constrpattern
+	  somatch               -> is_matching
+          dest_somatch          -> matches
+
+        Tacticals
+	  matches               -> gl_is_matching
+          dest_match            -> gl_matches
+	  suff                  -> utiliser sort_of_goal
+          lookup_eliminator     -> utiliser sort_of_goal pour le dernier arg
+
+        Divers
+          initial_sign     -> var_context
+
+        Sign
+          ids_of_sign      -> ids_of_var_context (or Environ.ids_of_context)
+          empty_sign       -> empty_var_context
+
+        Pfedit
+	  list_proofs      -> get_all_proof_names
+          get_proof        -> get_current_proof_name
+          abort_goal       -> abort_proof
+          abort_goals      -> abort_all_proofs
+          abort_cur_goal   -> abort_current_proof
+          get_evmap_sign   -> get_goal_context/get_current_goal_context
+          unset_undo       -> reset_undo
+
+        Proof_trees
+          mkGOAL           -> mk_goal
+
+        Declare
+  	  machine_constant ->   declare_constant (+ modifs)
+
+	ex-Trad, maintenant Pretyping
+          inh_cast_rel        -> Coercion.inh_conv_coerce_to
+          inh_conv_coerce_to  -> Coercion.inh_conv_coerce_to_fail
+	  ise_resolve1        -> understand, understand_type
+	  ise_resolve         -> understand_judgment, understand_type_judgment
+
+        ex-Tradevar, maintenant Evarutil
+          mt_tycon            -> empty_tycon
+
+        Recordops
+          struc_info          -> find_structure
+
+Changements dans les inductifs
+------------------------------
+Nouveaux types "constructor" et "inductive" dans Term
+La plupart des fonctions de typage des inductives prennent maintenant
+un inductive au lieu d'un oonstr comme argument. Les seules fonctions
+à traduire un constr en inductive sont les find_rectype and co.
+
+Changements dans les grammaires
+-------------------------------
+
+ . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex
+
+ . attention : LIDENT -> IDENT  (les identificateurs n'ont pas de
+                                 casse particulière dans Coq)
+
+ . Le mot "command" est remplacé par "constr" dans les noms de
+ fichiers, noms de modules et non-terminaux relatifs au parsing des
+ termes; aussi les changements suivants "COMMAND"/"CONSTR" dans
+ g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml*
+
+ . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n
+   passent en minuscule Identifier, Constr, ...
+ 
+ . Plusieurs parsers ont changé de format (ex: sortarg)
+
+Changements dans le pretty-printing
+-----------------------------------
+
+ . Découplage de la traduction de constr -> rawconstr (dans detyping)
+    et de rawconstr -> ast (dans termast)
+ . Déplacement des options d'affichage de printer vers termast
+ . Déplacement des réaiguillage d'univers du pp de printer vers esyntax
+
+	
+Changements divers
+------------------
+
+ . il n'y a plus de script coqtop => coqtop et coqtop.byte sont
+   directement le résultat du link du code
+   => debuggage et profiling directs
+
+ . il n'y a plus d'installation locale dans bin/$ARCH
+ 
+ . #use "include.ml"  =>  #use "include"
+   go()               =>  loop()
+
+ . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
+   de temps
diff --git a/dev/db b/dev/db
new file mode 100644
index 00000000..44effd77
--- /dev/null
+++ b/dev/db
@@ -0,0 +1,35 @@
+load_printer "gramlib.cma"
+load_printer "top_printers.cmo"
+install_printer Top_printers.prid
+install_printer Top_printers.prlab
+install_printer Top_printers.prmsid
+install_printer Top_printers.prmbid
+install_printer Top_printers.prdir
+install_printer Top_printers.prmp
+install_printer Top_printers.prkn
+install_printer Top_printers.prsp
+install_printer Top_printers.prqualid
+install_printer Top_printers.prast
+install_printer Top_printers.prastpat
+install_printer Top_printers.prastpatl
+
+install_printer Top_printers.pppattern
+install_printer Top_printers.pprawterm
+
+install_printer Top_printers.ppterm
+install_printer Top_printers.print_uni
+install_printer Top_printers.pp_universes
+install_printer Top_printers.pptype
+install_printer Top_printers.prj
+
+install_printer Top_printers.prgoal
+install_printer Top_printers.prsigmagoal
+install_printer Top_printers.pproof
+install_printer Top_printers.prevd
+install_printer Top_printers.prevc
+install_printer Top_printers.prwc
+install_printer Top_printers.prclenv
+
+install_printer Top_printers.pptac
+install_printer Top_printers.pr_obj                                                     
+
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
new file mode 100644
index 00000000..cee94d47
--- /dev/null
+++ b/dev/db_printers.ml
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+open Pp
+open Names
+
+let pp s = pp (hov 0 s)
+
+let prid id = Format.print_string (string_of_id id)
+let prsp sp = Format.print_string (string_of_path sp)
+
+
diff --git a/dev/deboguage.txt b/dev/deboguage.txt
new file mode 100644
index 00000000..eea7a0bc
--- /dev/null
+++ b/dev/deboguage.txt
@@ -0,0 +1,30 @@
+
+Debuggage
+=========
+
+   dans Emacs. nécessite le mode tuareg.
+   Coq doit être configuré avec -debug et -local (./configure -debug -local)
+
+   1. M-x camldebug
+   2. spécifier le binaire coqtop.byte
+   3. spécifier dev/ocamldebug-v7
+   4. source db  (pour avoir les pretty-printers)
+   5. poser ses points d'arrêts avec C-x C-a C-b (penser "add breakpoint")
+      directement dans le source ocaml
+   6. ensuite voir le man d'ocamldebug
+         run
+	 step
+	 next
+	 last
+	 print x
+	 ...
+
+
+Profiling
+=========
+
+   Coq doit être configuré avec -profile
+
+   1. Lancer Coq en natif, qui doit terminer normalement (utiliser Quit
+      ou l'option -batch)
+   2. gprof ./coqtop gmon.out
diff --git a/dev/debugging.txt b/dev/debugging.txt
new file mode 100644
index 00000000..d3fbf48a
--- /dev/null
+++ b/dev/debugging.txt
@@ -0,0 +1,50 @@
+
+Debugging from Coq toplevel using Caml trace mechanism
+======================================================
+
+  1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte)
+  2. Access Ocaml toplevel using vernacular command 'Drop.'
+  3. Install load paths and pretty printers for terms, idents, ... using
+     Ocaml command '#use "base_include";;' (use '#use "include";;' for a rawer
+     term pretty printer)
+  4. Use #trace to tell which function(s) to trace
+  5. Go back to Coq toplevel with 'go();;'
+  6. Test your Coq command and observe the result of tracing your functions
+  7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;'
+
+Debugging from Caml debugger
+============================
+
+   Needs tuareg mode in Emacs
+   Coq must be configured with -debug and -local (./configure -debug -local)
+
+   1. M-x camldebug
+   2. give the binary name coqtop.byte
+   3. give dev/ocamldebug-v7
+   4. source db  (to get pretty-printers)
+   5. add breakpoints with C-x C-a C-b from the buffer displaying the ocaml
+      source
+   6. get more help from ocamldebug manual
+         run
+	 step
+         back
+         start
+	 next
+	 last
+	 print x (abbreviated into p x)
+	 ...
+   7. some hints: 
+
+   - To debug a failure/error/anomaly, add a breakpoint in
+     Vernacinterp.call just before "if !Options.debug" then go "back" to
+     find where the failure/error/anomaly has been raised
+   - If "source db" fails, first recompile top_printers.ml with
+     "make dev/top_printers.cmo"
+
+Profiling
+=========
+
+   Coq must be configured with option -profile
+
+   1. Run native Coq which must end normally (use Quit or option -batch)
+   2. gprof ./coqtop gmon.out
diff --git a/dev/header b/dev/header
new file mode 100644
index 00000000..57945e47
--- /dev/null
+++ b/dev/header
@@ -0,0 +1,7 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
diff --git a/dev/include b/dev/include
new file mode 100644
index 00000000..eb370a5d
--- /dev/null
+++ b/dev/include
@@ -0,0 +1,35 @@
+
+(* File to include to install the pretty-printers in the ocaml toplevel *)
+
+#cd ".";;
+#use "base_include";;
+
+#install_printer  (* ast *)  prast;;
+#install_printer  (* pat *)  prastpat;;
+#install_printer  (* patlist *)  prastpatl;;
+
+#install_printer  (* pattern *) pppattern;;
+#install_printer  (* rawconstr *) pprawterm;;
+
+#install_printer  (* constr *) ppterm;;
+#install_printer  (* constr_substituted *) ppsterm;; 
+#install_printer  (* universe *)  print_uni;;
+#install_printer  (* universes *)  pp_universes;;
+#install_printer  (* type_judgement*) pptype;;
+#install_printer  (* judgement*) prj;;
+
+#install_printer  (* goal *)  prgoal;;
+#install_printer  (* sigma goal *)  prsigmagoal;;
+#install_printer  (* proof *)  pproof;;
+#install_printer  (* global_constraints *)  prevd;;
+#install_printer  (* readable_constraints *)  prevc;;
+#install_printer  (* walking_constraints *)  prwc;;
+#install_printer  (* clenv *) prclenv;;
+#install_printer  (* env *) ppenv;;
+
+#install_printer  (* tactic *) pptac;;
+#install_printer  (* object *) pr_obj;;
+#install_printer  (* global_reference *) prglobal;;
+
+#install_printer  (* fconstr *) ppfconstr;;
+
diff --git a/dev/objects.el b/dev/objects.el
new file mode 100644
index 00000000..b3a2694d
--- /dev/null
+++ b/dev/objects.el
@@ -0,0 +1,153 @@
+(defun add-survive-module nil
+  (interactive)
+  (query-replace-regexp 
+   "
+\\([ 	]*\\)\\(Summary\.\\)?survive_section"
+   "
+\\1\\2survive_module = false;
+\\1\\2survive_section")
+  )
+
+(global-set-key [f2] 'add-survive-module)
+
+; functions to change old style object declaration to new style
+
+(defun repl-open nil
+  (interactive)
+  (query-replace-regexp 
+   "open_function\\([ 	]*\\)=\\([ 	]*\\)cache_\\([a-zA-Z0-9'_]*\\)\\( *\\);" 
+   "open_function\\1=\\2(fun i o -> if i=1 then cache_\\3 o)\\4;") 
+  )
+
+(global-set-key [f6] 'repl-open)
+
+(defun repl-load nil
+  (interactive)
+  (query-replace-regexp 
+   "load_function\\([ 	]*\\)=\\([ 	]*\\)cache_\\([a-zA-Z0-9'_]*\\)\\( *\\);" 
+   "load_function\\1=\\2(fun _ -> cache_\\3)\\4;") 
+  )
+
+(global-set-key [f7] 'repl-load)
+
+(defun repl-decl nil
+  (interactive)
+  (query-replace-regexp
+   "\\(Libobject\.\\)?declare_object[ 
+	]*([ 	]*\\(.*\\)[ 
+	]*,[ 	]*
+\\([ 	]*\\){\\([ 	]*\\)\\([^ ][^}]*\\)}[ 	]*)"
+
+   "\\1declare_object {(\\1default_object \\2) with
+\\3 \\4\\5}")
+;   "|$1=\\1|$2=\\2|$3=\\3|$4=\\4|")
+)
+
+(global-set-key [f9] 'repl-decl)
+
+; eval the above and try f9 f6 f7 on the following:
+
+let (inThing,outThing) =
+  declare_object
+    ("THING", 
+     { load_function = cache_thing;
+       cache_function = cache_thing;
+       open_function = cache_thing;
+       export_function = (function x -> Some x)
+     })
+
+
+;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+; functions helping writing non-copying substitutions
+
+(defun make-subst (name)
+  (interactive "s")
+  (defun f (l)
+    (save-excursion
+      (query-replace-regexp
+       (concat "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*" 
+	       (car l) 
+	       "\\([ 	]*;\\|[ 	
+]*\}\\)")
+       (concat "let \\1\' = " (cdr l) " " name "\\1 in"))
+      )
+    )
+  (mapcar 'f '(("constr"."subst_mps subst") 
+	       ("Coqast.t"."subst_ast subst") 
+	       ("Coqast.t list"."list_smartmap (subst_ast subst)") 
+	       ("'pat"."subst_pat subst") 
+	       ("'pat unparsing_hunk"."subst_hunk subst_pat subst")
+	       ("'pat unparsing_hunk list"."list_smartmap (subst_hunk subst_pat subst)") 
+	       ("'pat syntax_entry"."subst_syntax_entry subst_pat subst")
+	       ("'pat syntax_entry list"."list_smartmap (subst_syntax_entry subst_pat subst)") 
+	       ("constr option"."option_smartmap (subst_mps subst)")
+	       ("constr list"."list_smartmap (subst_mps subst)")
+	       ("constr array"."array_smartmap (subst_mps subst)")
+	       ("constr_pattern"."subst_pattern subst")
+	       ("constr_pattern option"."option_smartmap (subst_pattern subst)")
+	       ("constr_pattern array"."array_smartmap (subst_pattern subst)")
+	       ("constr_pattern list"."list_smartmap (subst_pattern subst)")
+	       ("global_reference"."subst_global subst")
+	       ("extended_global_reference"."subst_ext subst")
+	       ("obj_typ"."subst_obj subst")
+	       )
+	  )
+  )
+
+
+(global-set-key [f2] 'make-subst)
+
+(defun make-if (name)
+  (interactive "s")
+  (save-excursion
+    (query-replace-regexp
+     "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*['a-zA-z_. ]*\\(;\\|[ 	
+]*\}\\)"
+     (concat "&& \\1\' == " name "\\1")
+     )
+    )
+  )
+
+(global-set-key [f4] 'make-if)
+
+(defun make-record nil
+  (interactive)
+  (save-excursion 
+    (query-replace-regexp
+     "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*['a-zA-z_. ]*\\(;\\|[ 	
+]*\}\\)"
+     (concat "\\1 = \\1\' ;")
+     )
+    )
+  )
+
+(global-set-key [f5] 'make-record)
+
+(defun make-prim nil
+  (interactive)
+  (save-excursion (query-replace-regexp "\\<[a-zA-Z'_0-9]*\\>" "\\&'"))
+  )
+
+(global-set-key [f6] 'make-prim)
+
+
+; eval the above, yank the text below and do 
+; paste f2 morph.
+; paste f4 morph.
+; paste f5
+
+      lem : constr;
+      profil : bool list;
+      arg_types : constr list;
+      lem2 : constr option                                                      }
+
+
+; and you almost get   Setoid_replace.subst_morph  :)
+
+; and now f5 on this:
+
+   (ref,(c1,c2))
+
+
+
diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-v7.template
new file mode 100644
index 00000000..96c53192
--- /dev/null
+++ b/dev/ocamldebug-v7.template
@@ -0,0 +1,41 @@
+#!/bin/sh
+
+# wrap around ocamldebug for Coq
+
+export COQTOP=COQTOPDIRECTORY
+export COQLIB=COQLIBDIRECTORY
+export COQTH=$COQLIB/theories
+CAMLBIN=CAMLBINDIRECTORY
+OCAMLDEBUG=$CAMLBIN/ocamldebug
+export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
+
+args=""
+coqdebug="no"
+for op in $*
+    do case `basename $op` in
+	coq-debug-programs.out) 
+	    coqdebug="yes"
+	    args="-is programs.coq";;
+	*coq*) coqdebug="yes";;
+       esac
+done
+
+case $coqdebug in
+    yes)
+	exec $OCAMLDEBUG \
+	-I $CAMLP4LIB \
+	-I $COQTOP/config \
+	-I $COQTOP/lib -I $COQTOP/kernel \
+	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
+        -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
+	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
+	-I $COQTOP/translate \
+        -I $COQTOP/contrib/correctness \
+        -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
+        -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/graphs \
+        -I $COQTOP/contrib/interface  -I $COQTOP/contrib/jprover \
+        -I $COQTOP/contrib/omega      -I $COQTOP/contrib/romega \
+        -I $COQTOP/contrib/ring       -I $COQTOP/contrib/xml \
+	$* $args;;
+    *) exec $OCAMLDEBUG $*;;
+esac
diff --git a/dev/style.txt b/dev/style.txt
new file mode 100644
index 00000000..2e597dc4
--- /dev/null
+++ b/dev/style.txt
@@ -0,0 +1,49 @@
+
+<< L'uniformité du style est plus importante que le style lui-même. >>
+(Kernigan & Pike, The Practice of Programming)
+
+Mode Emacs
+==========
+   Tuareg, que l'on trouve ici :  http://www.prism.uvsq.fr/~acohen/tuareg/
+
+   avec le réglage suivant :     (setq tuareg-in-indent 2)
+
+Types récursifs et filtrages
+============================
+   Une barre de séparation y compris sur le premier constructeur
+
+type t =
+  | A 
+  | B of machin
+
+match expr with
+  | A -> ...
+  | B x -> ...
+
+
+Conditionnelles
+===============
+  if condition then
+    premier-cas
+  else
+    deuxieme-cas
+
+  Si effets de bord dans les branches, utilisez begin ... end et non des
+  parenthèses i.e.
+
+  if condition then begin
+    instr1;
+    instr2
+  end else begin
+    instr3;
+    instr4
+  end
+    
+  Si la première branche lève une exception, évitez le else i.e.
+
+    if condition then                     if condition then error "machin";
+      error "machin"          ----->      suite
+    else
+      suite
+
+  
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
new file mode 100644
index 00000000..7f92d64c
--- /dev/null
+++ b/dev/top_printers.ml
@@ -0,0 +1,303 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Printers for the ocaml toplevel. *)
+
+open System
+open Pp
+open Ast
+open Names
+open Libnames
+open Nameops
+open Sign
+open Univ
+open Proof_trees
+open Environ
+open Printer
+open Refiner
+open Tacmach
+open Term
+open Termops
+open Clenv
+open Cerrors
+
+let _ = Constrextern.print_evar_arguments := true
+
+let pP s = pp (hov 0 s)
+
+let prast c = pp(print_ast c)
+
+let prastpat c = pp(print_astpat c)
+let prastpatl c = pp(print_astlpat c)
+let ppterm x = pp(prterm x)
+let ppsterm x = ppterm (Declarations.force x)
+let ppterm_univ x = Constrextern.with_universes ppterm x
+let pprawterm = (fun x -> pp(pr_rawterm x))
+let pppattern = (fun x -> pp(pr_pattern x))
+let pptype = (fun x -> pp(prtype x))
+
+let safe_prglobal = function 
+  | ConstRef kn -> pp (str "CONSTREF(" ++ pr_kn kn ++ str ")")
+  | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
+			  int i ++ str ")")
+  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
+				      int i ++ str "," ++ int j ++ str ")")
+  | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
+
+let prglobal x = try pp(pr_global x) with _ -> safe_prglobal x
+
+let prid id = pp (pr_id id)
+let prlab l = pp (pr_lab l)
+
+let prmsid msid = pp (str (debug_string_of_msid msid))
+let prmbid mbid = pp (str (debug_string_of_mbid mbid))
+
+let prdir dir = pp (pr_dirpath dir)
+
+let prmp mp = pp(str (string_of_mp mp))
+let prkn kn = pp(pr_kn kn)
+
+let prsp sp = pp(pr_sp sp)
+
+let prqualid qid = pp(pr_qualid qid)
+
+let prconst (sp,j) =
+    pp (str"#" ++ pr_kn sp ++ str"=" ++ prterm j.uj_val)
+
+let prvar ((id,a)) =
+    pp (str"#" ++ pr_id id ++ str":" ++ prterm a)
+
+let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t)
+
+let prj j = pp (genprj prjudge j)
+
+let prgoal g = pp(prgl g)
+
+let prsigmagoal g = pp(prgl (sig_it g))
+
+let prgls gls = pp(pr_gls gls)
+
+let prglls glls = pp(pr_glls glls)
+
+let pproof p = pp(print_proof Evd.empty empty_named_context p)
+
+let prevd evd = pp(pr_decls evd)
+
+let prevc evc = pp(pr_evc evc)
+
+let prwc wc = pp(pr_evc wc)
+
+let prclenv clenv = pp(pr_clenv clenv)
+
+let print_uni u = (pp (pr_uni u))
+
+let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]")
+
+let ppenv e = pp
+  (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
+   str "[" ++ pr_rel_context e (rel_context e) ++ str "]")
+
+let pptac = (fun x -> pp(Pptactic.pr_glob_tactic x))
+
+let pr_obj obj = Format.print_string (Libobject.object_tag obj)
+
+let cnt = ref 0
+
+let constr_display csr =
+  let rec term_display c = match kind_of_term c with
+  | Rel n -> "Rel("^(string_of_int n)^")"
+  | Meta n -> "Meta("^(string_of_int n)^")"
+  | Var id -> "Var("^(string_of_id id)^")"
+  | Sort s -> "Sort("^(sort_display s)^")"
+  | Cast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")"
+  | Prod (na,t,c) ->
+      "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
+  | Lambda (na,t,c) ->
+      "Lambda("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
+  | LetIn (na,b,t,c) ->
+      "LetIn("^(name_display na)^","^(term_display b)^","
+      ^(term_display t)^","^(term_display c)^")"
+  | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
+  | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
+  | Const c -> "Const("^(string_of_kn c)^")"
+  | Ind (sp,i) ->
+      "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")"
+  | Construct ((sp,i),j) ->
+      "MutConstruct(("^(string_of_kn sp)^","^(string_of_int i)^"),"
+      ^(string_of_int j)^")"
+  | Case (ci,p,c,bl) ->
+      "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
+      ^(array_display bl)^")"
+  | Fix ((t,i),(lna,tl,bl)) ->
+      "Fix(([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="")
+        then (";"^i) else "")) t "")^"|],"^(string_of_int i)^"),"
+      ^(array_display tl)^","
+      ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="")
+        then (";"^i) else "")) lna "")^","
+      ^(array_display bl)^")"
+  | CoFix(i,(lna,tl,bl)) ->
+      "CoFix("^(string_of_int i)^"),"
+      ^(array_display tl)^","
+      ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="")
+        then (";"^i) else "")) lna "")^","
+      ^(array_display bl)^")"
+
+  and array_display v =
+    "[|"^
+    (Array.fold_right
+       (fun x i -> (term_display x)^(if not(i="") then (";"^i) else ""))
+       v "")^"|]"
+
+  and sort_display = function
+    | Prop(Pos) -> "Prop(Pos)"
+    | Prop(Null) -> "Prop(Null)"
+    | Type u ->
+	incr cnt; pp (str "with " ++ int !cnt ++ pr_uni u ++ fnl ());
+	"Type("^(string_of_int !cnt)^")"
+
+  and name_display = function
+    | Name id -> "Name("^(string_of_id id)^")"
+    | Anonymous -> "Anonymous"
+
+  in
+    msg (str (term_display csr) ++fnl ())
+
+open Format;;
+
+let print_pure_constr csr =
+  let rec term_display c = match kind_of_term c with
+  | Rel n -> print_string "#"; print_int n
+  | Meta n -> print_string "Meta("; print_int n; print_string ")"
+  | Var id -> print_string (string_of_id id)
+  | Sort s -> sort_display s
+  | Cast (c,t) -> open_hovbox 1;
+      print_string "("; (term_display c); print_cut();
+      print_string "::"; (term_display t); print_string ")"; close_box()
+  | Prod (Name(id),t,c) ->
+      open_hovbox 1;
+      print_string"("; print_string (string_of_id id); 
+      print_string ":"; box_display t; 
+      print_string ")"; print_cut(); 
+      box_display c; close_box()
+  | Prod (Anonymous,t,c) ->
+      print_string"("; box_display t; print_cut(); print_string "->";
+      box_display c; print_string ")"; 
+  | Lambda (na,t,c) ->
+      print_string "["; name_display na;
+      print_string ":"; box_display t; print_string "]";
+      print_cut(); box_display c; 
+  | LetIn (na,b,t,c) ->
+      print_string "["; name_display na; print_string "="; 
+      box_display b; print_cut();
+      print_string ":"; box_display t; print_string "]";
+      print_cut(); box_display c; 
+  | App (c,l) -> 
+      print_string "("; 
+      box_display c; 
+      Array.iter (fun x -> print_space (); box_display x) l;
+      print_string ")"
+  | Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{";
+      Array.iter (fun x -> print_space (); box_display x) l;
+      print_string"}"
+  | Const c -> print_string "Cons(";
+      sp_display c;
+      print_string ")"
+  | Ind (sp,i) ->
+      print_string "Ind(";
+      sp_display sp;
+      print_string ","; print_int i;
+      print_string ")"
+  | Construct ((sp,i),j) ->
+      print_string "Constr(";
+      sp_display sp;
+      print_string ",";
+      print_int i; print_string ","; print_int j; print_string ")"
+  | Case (ci,p,c,bl) ->
+      open_vbox 0;
+      print_string "<"; box_display p; print_string ">";
+      print_cut(); print_string "Case";
+      print_space(); box_display c; print_space (); print_string "of";
+      open_vbox 0;
+      Array.iter (fun x ->  print_cut();  box_display x) bl;
+      close_box();
+      print_cut(); 
+      print_string "end"; 
+      close_box()
+  | Fix ((t,i),(lna,tl,bl)) ->
+      print_string "Fix("; print_int i; print_string ")"; 
+      print_cut();
+      open_vbox 0;
+      let rec print_fix () =
+        for k = 0 to Array.length tl do
+	  open_vbox 0;
+	  name_display lna.(k); print_string "/"; 
+	  print_int t.(k); print_cut(); print_string ":";
+	  box_display tl.(k) ; print_cut(); print_string ":=";
+	  box_display bl.(k); close_box ();
+	  print_cut()
+        done
+      in print_string"{"; print_fix(); print_string"}"
+  | CoFix(i,(lna,tl,bl)) ->
+      print_string "CoFix("; print_int i; print_string ")"; 
+      print_cut();
+      open_vbox 0;
+      let rec print_fix () =
+        for k = 0 to Array.length tl do
+          open_vbox 1;
+	  name_display lna.(k);  print_cut(); print_string ":";
+	  box_display tl.(k) ; print_cut(); print_string ":=";
+	  box_display bl.(k); close_box ();
+	  print_cut();
+        done
+      in print_string"{"; print_fix (); print_string"}"
+
+  and box_display c = open_hovbox 1; term_display c; close_box()
+
+  and sort_display = function
+    | Prop(Pos) -> print_string "Set"
+    | Prop(Null) -> print_string "Prop"
+    | Type u -> open_hbox();
+	print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
+
+  and name_display = function
+    | Name id -> print_string (string_of_id id)
+    | Anonymous -> print_string "_"
+(* Remove the top names for library and Scratch to avoid long names *)
+  and sp_display sp = 
+(*    let dir,l = decode_kn sp in
+    let ls = 
+      match List.rev (List.map string_of_id (repr_dirpath dir)) with 
+          ("Top"::l)-> l
+	| ("Coq"::_::l) -> l 
+	| l             -> l
+    in  List.iter (fun x -> print_string x; print_string ".") ls;*)
+      print_string (string_of_kn sp)
+
+  in
+     box_display csr; print_flush()
+(*
+let _ =
+  Vernacentries.add "PrintConstr"
+    (function
+       | [VARG_CONSTR c] -> 
+	   (fun () ->
+              let (evmap,sign) = Command.get_current_context () in
+  	      constr_display (Constrintern.interp_constr evmap sign c))
+       | _ -> bad_vernac_args "PrintConstr")
+
+let _ =
+  Vernacentries.add "PrintPureConstr"
+    (function
+       | [VARG_CONSTR c] -> 
+	   (fun () ->
+              let (evmap,sign) = Command.get_current_context () in
+  	      print_pure_constr (Constrintern.interp_constr evmap sign c))
+       | _ -> bad_vernac_args "PrintPureConstr")
+*)
+
+let ppfconstr c = ppterm (Closure.term_of_fconstr c)
diff --git a/dev/translate.txt b/dev/translate.txt
new file mode 100644
index 00000000..5b372c96
--- /dev/null
+++ b/dev/translate.txt
@@ -0,0 +1,495 @@
+
+                 How to use the translator
+                 =========================
+
+       (temporary version to be included in the official
+           TeX document describing the translator)
+
+The translator is a smart, robust and powerful tool to improve the
+readibility of your script. The current document describes the
+possibilities of the translator.
+
+In case of problem recompiling the translated files, don't waste time
+to modify the translated file by hand, read first the following
+document telling on how to modify the original files to get a smooth
+uniform safe translation. All 60000 lines of Coq lines on our
+user-contributions server have been translated without any change
+afterwards, and 0,5 % of the lines of the original files (mainly
+notations) had to be modified beforehand to get this result.
+
+Table of contents
+-----------------
+
+I) Implicit Arguments
+ 1) Strict Implicit Arguments 
+ 2) Implicit Arguments in standard library
+
+II) Notations
+ 1) Translating a V7 notation as it was
+ 2) Translating a V7 notation which conflicts with the new syntax
+  a) Associativity conflicts
+  b) Conflicts with other notations
+   b1) A notation hides another notation 
+   b2) A notation conflicts with the V8 grammar
+   b3) My notation is already defined at another level
+  c) How to use V8only with Distfix ?
+  d) Can I overload a notation in V8, e.g. use "*" and "+" ?
+ 3) Using the translator to have simplest notations
+ 4) Setting the translator to automatically use new notations that
+    wasn't used in old syntax
+ 5) Defining a construction and its notation simultaneously
+
+III) Various pitfalls
+ 1) New keywords
+ 2) Old "Case" and "Match"
+ 3) Change of definition or theorem names
+ 4) Change of tactic names
+
+---------------------------------------------------------------------
+
+I) Implicit Arguments
+   ------------------
+
+1) Strict Implicit Arguments 
+
+  "Set Implicit Arguments" changes its meaning in V8: the default is
+to turn implicit only the arguments that are _strictly_ implicit (or
+rigid), i.e. that remains inferable whatever the other arguments
+are. E.g "x" inferable from "P x" is not strictly inferable since it
+can disappears if "P" is instanciated by a term which erase "x".
+
+  To respect the old semantics, the default behaviour of the
+translator is to replace each occurrence "Set Implicit Arguments" by
+
+  Set Implicit Arguments.
+  Unset Strict Implicits.
+
+  However, you may wish to adopt the new semantics of "Set Implicit
+Arguments" (for instance because you think that the choice of
+arguments it setsimplicit is more "natural" for you). In this case,
+add the option -strict-implicit to the translator.
+
+  Warning: Changing the number of implicit arguments can break the
+notations.  Then use the V8only modifier of Notations.
+
+2) Implicit Arguments in standard library
+
+  Main definitions of standard library have now implicit
+arguments. These arguments are dropped in the translated files. This
+can exceptionally be a source of incompatibilities which has to be
+solved by hand (it typically happens for polymorphic functions applied
+to "nil" or "None").
+
+II) Notations
+    ---------
+
+  Grammar (on constr) and Syntax are no longer supported. Replace them by
+Notation before translation.
+
+  Precedence levels are now from 0 to 200. In V8, the precedence and
+associativity of an operator cannot be redefined. Typical level are
+(refer to the chapter on notations in the Reference Manual for the
+full list):
+
+  <-> : 95                    (no associativity)
+  -> : 90                     (right associativity)
+  \/ : 85                     (right associativity)
+  /\ : 80                     (right associativity)
+  ~ : 75                      (right associativity)
+  =, <, >, <=, >=, <> : 70    (no associativity)
+  +, - : 50                   (left associativity)
+  *, / : 40                   (left associativity)
+  ^ : 30                      (right associativity)
+
+1) Translating a V7 notation as it was
+
+  By default, the translator keeps the associativity given in V7 while
+the levels are mapped according to the following table:
+ 
+  the V7 levels             [  0;  1;  2;  3;  4;  5;  6;  7;  8;  9;  10]
+  are resp. mapped in V8 to [  0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100]
+  with predefined assoc     [ No;  L;  R;  L;  L; No;  R;  R;  R; No;   L]
+
+  If this is OK for you, just simply apply the translator.
+
+2) Translating a V7 notation which conflicts with the new syntax
+
+a) Associativity conflict
+
+  Since the associativity of the levels obtained by translating a V7
+level (as shown on table above) cannot be changed, you have to choose
+another level with a compatible associativity.
+
+  You can choose any level between 0 and 200, knowing that the
+standard operators are already set at the levels shown on the list
+above. 
+
+Example 1: Assume you have a notation
+
+Infix NONA 2 "=_S" my_setoid_eq.
+
+By default, the translator moves it to level 30 which is right
+associative, hence a conflict with the expected no associativity.
+
+To solve the problem, just add the "V8only" modifier to reset the
+level and enforce the associativity as follows:
+
+Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).
+
+The translator now knows that it has to translate "=_S" at level 70
+with no associativity.
+
+Rem: 70 is the "natural" level for relations, hence the choice of 70
+here, but any other level accepting a no-associativity would have been
+OK.
+
+Example 2: Assume you have a notation
+
+Infix RIGHTA 1 "o" my_comp.
+
+By default, the translator moves it to level 20 which is left
+associative, hence a conflict with the expected right associativity.
+
+To solve the problem, just add the "V8only" modifier to reset the
+level and enforce the associativity as follows:
+
+Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).
+
+The translator now knows that it has to translate "o" at level 20
+which has the correct "right associativity".
+
+Rem: We assumed here that the user wants a strong precedence for
+composition, in such a way, say, that "f o g + h" is parsed as
+"(f o g) + h". To get "o" binding less than the arithmetical operators,
+an appropriated level would have been close of 70, and below, e.g. 65.
+
+b) Conflicts with other notations
+
+Since the new syntax comes with new keywords and new predefined
+symbols, new conflicts can occur. Again, you can use the option V8only
+to inform the translator of the new syntax to use.
+
+b1) A notation hides another notation 
+
+Rem: use Print Grammar constr in V8 to diagnose the overlap and see the
+section on factorization in the chapter on notations of the Reference
+Manual for hints on how to factorize.
+
+Example:
+
+Notation "{ x }" := (my_embedding x) (at level 1).
+
+overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at
+level 99. The conflicts can be solved by left-factorizing the notation
+as follows:
+
+Notation "{ x }" := (my_embedding x) (at level 1)
+  V8only (at level 0, x at level 99).
+
+b2) A notation conflicts with the V8 grammar.
+
+Again, use the V8only modifier to tell the translator to automatically
+take in charge the new syntax.
+
+Example:
+
+Infix 3 "@" app.
+
+Since "@" is used in the new syntax for deactivating the implicit
+arguments, another symbol has to be used, e.g. "@@". This is done via
+the V8only option as follows:
+
+Infix 3 "@" app V8only "@@" (at level 40, left associativity).
+
+or, alternatively by
+
+Notation "x @ y" := (app x y) (at level 3, left associativity)
+  V8only "x @@ y" (at level 40, left associativity).
+
+b3) My notation is already defined at another level (or with another
+associativity)
+
+In V8, the level and associativity of a given notation can no longer
+be changed. Then, either you adopt the standard reserved levels and
+associativity for this notation (as given on the list above) or you
+change your notation.
+
+- To change the notation, follow the directions in section b2.
+
+- To adopt the standard level, just use V8only without any argument.
+
+Example.
+
+Infix 6 "*" my_mult.
+
+is not accepted as such in V8. Write
+
+Infix 6 "*" my_mult V8only.
+
+to tell the translator to use "*" at the reserved level (i.e. 40 with
+left associativity). Even better, use interpretation scopes (look at
+the Reference Manual).
+
+c) How to use V8only with Distfix ?
+
+You can't, use Notation instead of Distfix.
+
+d) Can I overload a notation in V8, e.g. use "*" and "+" for my own
+algebraic operations ?
+
+Yes, using interpretation scopes (see the corresponding chapter in the
+Reference Manual).
+
+3) Using the translator to have simplest notations
+
+Thanks to the new syntax, * has now the expected left associativity,
+and the symbols <, >, <= and >= are now available.
+
+Thanks to the interpretation scopes, you can overload the
+interpretation of these operators with the default interpretation
+provided in Coq.
+
+This may be a motivation to use the translator to automatically change
+the notations while switching to the new syntax.
+
+See sections b) and d) above for examples.
+
+4) Setting the translator to automatically use new notations that
+wasn't used in old syntax
+
+Thanks to the "Notation" mechanism, defining symbolic notations is
+simpler than in the previous versions of Coq.
+
+Thanks to the new syntax and interpretation scopes, new symbols and
+overloading is available.
+
+This may be a motivation for using the translator to automatically change
+the notations while switching to the new syntax.
+
+Use for that the commands V8Notation and V8Infix.
+
+Examples:
+
+V8Infix "==>" my_relation (at level 65, right associativity).
+
+tells the translator to write an infix "==>" instead of my_relation in
+the translated files.
+
+V8Infix ">=" my_ge.
+
+tells the translator to write an infix ">=" instead of my_ge in the
+translated files and that the level and associativity are the standard
+one (as defined in the chart above).
+
+V8Infix ">=" my_ge : my_scope.
+
+tells the translator to write an infix ">=" instead of my_ge in the
+translated files, that the level and associativity are the standard
+one (as defined in the chart above), but only if scope my_scope is
+open or if a delimiting key is available for "my_scope" (see the
+Reference Manual).
+
+5) Defining a construction and its notation simultaneously
+
+This is permitted by the new syntax. Look at the Reference Manual for
+explanation. The translator is not fully able to take this in charge...
+
+III) Various pitfalls
+    ----------------
+
+1) New keywords
+
+  The following identifiers are new keywords
+
+  "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then";
+  "else"; "return"; "mod"; "at"; "let"; "_"; ".("
+
+  The translator automatically add a "_" to names clashing with a
+keyword, except for files. Hence users may need to rename the files
+whose name clashes with a keyword.
+
+  Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type"
+  were already keywords
+
+2) Old "Case" and "Match"
+
+  "Case" and "Match" are normally automatically translated into
+  "match" or "match" and "fix", but sometimes it fails to do so. It
+  typically fails when the Case or Match is argument of a tactic whose
+  typing context is unknown because of a preceding Intro/Intros, as e.g. in 
+
+     Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
+
+  The solution is then to replace the invocation of the sequence of
+  tactics into several invocation of the elementary tactics as follows
+
+     Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
+          ^^^
+
+3) Change of definition or theorem names
+
+  Type "entier" from fast_integer.v is renamed into "N" by the
+translator. As a consequence, user-defined objects of same name "N"
+are systematically qualified even tough it may not be necessary.  The
+same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST
+TO GIVE].
+
+4) Change of tactics names
+
+  Since tactics names are now lowercase, this can clash with
+user-defined tactic definitions. To pally this, clashing names are
+renamed by adding an extra "_" to their name.
+
+======================================================================
+Main examples for new syntax
+----------------------------
+
+1) Constructions
+
+  Applicative terms don't any longer require to be surrounded by parentheses as
+e.g in
+
+  "x = f y -> S x = S (f y)"
+
+
+  Product is written
+
+     "forall x y : T, U"
+     "forall x y, U"
+     "forall (x y : T) z (v w : V), U"
+     etc.
+
+  Abstraction is written
+
+     "fun x y : T, U"
+     "fun x y, U"
+     "fun (x y : T) z (v w : V), U"
+     etc.
+
+  Pattern-matching is written
+
+     "match x with c1 x1 x2 => t | c2 y as z => u end"
+     "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end"
+     "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with
+         c1 x1 x2, _ => t | c2 y, d z => u end"
+
+     The last example is the new form of what was written
+
+    "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of
+         (c1 x1 x2) _ => t | (c2 y) (d z) => u end"
+
+  Pattern-matching of type with one constructors and no dependencies
+of the arguments in the resulting type can be written
+
+    "let (x,y,z) as u return P u := t in v"
+     
+  Local fixpoints are written
+
+    "fix f (n m:nat) z (x : X) {struct m} : nat := ...
+     with ..."
+
+    and "struct" tells which argument is structurally decreasing.
+
+  Explicitation of implicit arguments is written
+
+     "f @1:=u v @3:=w t"
+     "@f u v w t"
+
+2) Tactics
+
+  The main change is that tactics names are now lowercase. Besides
+this, the following renaming are applied:
+
+  "NewDestruct" -> "destruct"
+  "NewInduction" -> "induction"
+  "Induction" -> "simple induction"
+  "Destruct" -> "simple destruct"
+
+  For tactics with occurrences, the occurrences now comes after and
+  repeated use is separated by comma as in
+
+  "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4"
+  "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4"
+  "Simpl 1 3 e" -> "simpl e at 1 3"
+
+3) Tactic language
+
+  Definitions are now introduced with keyword "Ltac" (instead of
+"Tactic"/"Meta" "Definition") and are implicitly recursive
+("Recursive" is no longer used).
+
+  The new rule for distinguishing terms from ltac expressions is:
+
+  Write "ltac:" in front of any tactic in argument position and
+  "constr:" in front of any construction in head position
+
+4) Vernacular language
+
+a) Assumptions
+
+  The syntax for commands is mainly unchanged. Declaration of
+assumptions is now done as follows
+
+  Variable m : t.
+  Variables m n p : t.
+  Variables (m n : t) (u v : s) (w : r).
+  
+b) Definitions
+
+  Definitions are done as follows
+
+  Definition f m n : t := ... .
+  Definition f m n := ... .
+  Definition f m n := ... : t.
+  Definition f (m n : u) : t := ... .
+  Definition f (m n : u) := ... : t.
+  Definition f (m n : u) := ... .
+  Definition f a b (p q : v) r s (m n : t) : t := ... .
+  Definition f a b (p q : v) r s (m n : t) := ... .
+  Definition f a b (p q : v) r s (m n : t) := ... : t.
+
+c) Fixpoints
+
+  Fixpoints are done this way
+  
+  Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... .
+  Fixpoint f x : v := ... .
+  Fixpoint f (x : t) : v := ... .
+
+  It is possible to give a concrete notation to a fixpoint as follows
+
+  Fixpoint plus (n m:nat) {struct n} : nat as "n + m" :=
+    match n with
+    | O => m
+    | S p => S (p + m)
+    end.
+
+d) Inductive types
+
+  The syntax for inductive types is as follows
+
+  Inductive t (a b : u) (d : e) : v :=
+     c1 : w1 | c2 : w2 | ... .
+
+  Inductive t (a b : u) (d : e) : v :=
+     c1 : w1 | c2 : w2 | ... .
+
+  Inductive t (a b : u) (d : e) : v :=
+     c1 (x y : t) : w1 | c2 (z : r) : w2 | ... .
+
+  As seen in the last example, arguments of the constructors can be
+given before the colon. If the type itself is omitted (allowed only in
+case the inductive type has no real arguments), this yields an
+ML-style notation as follows
+
+  Inductive nat : Set := O | S (n:nat).
+  Inductive bool : Set := true | false.
+
+  It is even possible to define a syntax at the same time, as follows:
+
+  Inductive or (A B:Prop) : Prop as "A \/ B":=
+    | or_introl (a:A) : A \/ B 
+    | or_intror (b:B) : A \/ B.
+
+  Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B).
+  
diff --git a/dev/univdot b/dev/univdot
new file mode 100755
index 00000000..bb0dd2c8
--- /dev/null
+++ b/dev/univdot
@@ -0,0 +1,49 @@
+#!/bin/sh
+
+usage() {
+    echo ""
+    echo "usage: univdot [INPUT] [OUTPUT]"
+    echo ""
+    echo "takes the output of Dump Universes \"file\" command"
+    echo "and transforms it to the dot format"
+    echo ""
+    echo "Coq> Dump Universes \"univ.raw\"."
+    echo ""
+    echo "user@host> univdot univ.raw | dot -Tps > univ.ps" 
+    echo ""
+}
+    
+
+# these are dot edge attributes to draw arrows corresponding 
+# to > >= and = edges of the universe graph
+
+GT="[color=red]"
+GE="[color=blue]"
+EQ="[color=black]"
+
+
+# input/output redirection
+case $# in
+  0) ;;
+  1) case $1 in
+       -h|-help|--help) usage
+               exit 0 ;;
+       *) exec < $1 ;;
+     esac ;;
+  2) exec < $1 > $2 ;;
+  *) usage
+     exit 0;;
+esac
+
+
+# dot header
+echo 'digraph G {\
+  size="7.5,10" ;\
+  rankdir = TB ;'
+
+sed -e "s/^\([^ =>]\+\) > \([^ =>]\+\)/\1 -> \2 $GT/" \
+      -e "s/^\([^ =>]\+\) >= \([^ =>]\+\)/\1 -> \2 $GE/" \
+      -e "s/^\([^ =>]\+\) = \([^ =>]\+\)/\1 -> \2 $EQ/" \
+| sed -e "s/\./_/g" 
+
+echo "}"
\ No newline at end of file
diff --git a/dev/universes.txt b/dev/universes.txt
new file mode 100644
index 00000000..65c1e522
--- /dev/null
+++ b/dev/universes.txt
@@ -0,0 +1,32 @@
+How to debug universes?
+
+1. There is a command Dump Universes in Coq toplevel
+
+   Dump Universes.
+     prints the graph of universes in the form of constraints
+
+   Dump Universes "file".
+     produces the "file" containing universe constraints in the form
+       univ1 # univ2 ;
+     where # can be either > >= or =
+     
+   The file produced by the latter command can be transformed using
+   the script univdot to dot format.
+   For example
+
+   univdot file | dot -Tps > file.ps
+
+   produces a graph of universes in ps format. 
+   > arrows are red, >= blue, and = black.
+
+
+   *) for dot see http://www.research.att.com/sw/tools/graphviz/
+
+
+2. There is a printing option
+  
+   Termast.print_universes : bool ref
+
+   which, when set (in ocaml after Drop), makes all pretty-printed
+   Type's annotated with the name of the universe.
+