From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 4 Jul 2009 13:28:35 +0200
Subject: Imported Upstream version 8.2.pl1+dfsg

---
 CHANGES                                     |  47 +++++++
 COPYRIGHT                                   |  18 +--
 CREDITS                                     |  19 ++-
 Makefile                                    |  30 +++--
 Makefile.build                              |   6 +-
 Makefile.common                             |   3 +-
 Makefile.doc                                |  28 ++--
 Makefile.stage1                             |   1 +
 checker/safe_typing.ml                      |   2 +-
 config/coq_config.mli                       |   6 +-
 configure                                   |  22 +++-
 contrib/interface/depends.ml                |   8 +-
 contrib/subtac/subtac.ml                    |  14 +-
 contrib/subtac/subtac_cases.ml              | 192 +++++++---------------------
 contrib/subtac/subtac_classes.ml            |   4 +-
 contrib/subtac/subtac_command.ml            |   2 +-
 contrib/subtac/subtac_obligations.ml        |  27 ++--
 contrib/subtac/subtac_obligations.mli       |   5 +-
 contrib/subtac/subtac_pretyping.ml          |  13 +-
 contrib/subtac/subtac_pretyping.mli         |   3 +-
 contrib/subtac/subtac_utils.ml              |  24 ++--
 contrib/subtac/subtac_utils.mli             |   8 +-
 contrib/xml/proofTree2Xml.ml4               |   4 +-
 dev/base_include                            |   6 +
 doc/common/styles/html/simple/footer.html   |   2 +
 doc/common/styles/html/simple/header.html   |  13 ++
 doc/common/styles/html/simple/style.css     |  13 ++
 doc/stdlib/index-list.html.template         |  16 +--
 doc/stdlib/index-trailer.html               |   2 -
 ide/coq.ml                                  |   4 +-
 ide/coqide.ml                               |   8 +-
 ide/preferences.ml                          |   6 +-
 install.sh                                  |   2 +-
 kernel/environ.ml                           |  40 ++++--
 kernel/environ.mli                          |   9 +-
 kernel/mod_subst.ml                         |  20 +--
 kernel/modops.ml                            |   8 +-
 kernel/safe_typing.ml                       |   4 +-
 lib/util.ml                                 |   4 +-
 library/declare.ml                          |   6 +-
 library/declare.mli                         |   4 +-
 library/declaremods.ml                      |  90 ++++++-------
 library/impargs.ml                          |  56 ++++----
 library/impargs.mli                         |   4 +-
 library/lib.ml                              |  22 ++--
 library/lib.mli                             |   6 +-
 library/states.ml                           |   9 +-
 library/states.mli                          |   7 +-
 parsing/g_tactic.ml4                        |  11 +-
 parsing/g_vernac.ml4                        |  14 +-
 parsing/pcoq.ml4                            |   7 +-
 parsing/ppvernac.ml                         |   5 +-
 parsing/prettyp.ml                          |   7 +-
 parsing/printer.ml                          |  42 ++++--
 pretyping/cases.ml                          |  29 +++--
 pretyping/evarconv.ml                       |  10 +-
 pretyping/evarutil.ml                       |  49 ++++---
 pretyping/evarutil.mli                      |  12 +-
 pretyping/pretyping.ml                      |  10 +-
 pretyping/recordops.ml                      |   7 +-
 pretyping/termops.ml                        |  11 +-
 pretyping/termops.mli                       |   4 +-
 pretyping/typeclasses.ml                    |   4 +-
 pretyping/unification.ml                    |   6 +-
 proofs/clenvtac.ml                          |   3 +-
 proofs/evar_refiner.ml                      |  15 ++-
 proofs/evar_refiner.mli                     |   7 +-
 proofs/logic.ml                             |  29 +++--
 proofs/proof_type.ml                        |   6 +-
 proofs/proof_type.mli                       |   6 +-
 proofs/tacmach.ml                           |  14 +-
 proofs/tacmach.mli                          |   6 +-
 tactics/auto.ml                             | 101 ++++++++-------
 tactics/auto.mli                            |   3 +-
 tactics/class_tactics.ml4                   |  17 +--
 tactics/decl_proof_instr.ml                 |   4 +-
 tactics/equality.ml                         |   4 +-
 tactics/evar_tactics.ml                     |   8 +-
 tactics/evar_tactics.mli                    |   4 +-
 tactics/extraargs.ml4                       |   6 +-
 tactics/extraargs.mli                       |   4 +-
 tactics/hiddentac.ml                        |   6 +-
 tactics/hiddentac.mli                       |   4 +-
 tactics/refine.ml                           |  27 ++--
 tactics/tacinterp.ml                        |  46 ++++---
 tactics/tacinterp.mli                       |   5 +-
 tactics/tacticals.ml                        |   3 +-
 tactics/tactics.ml                          |  72 +++++++----
 test-suite/bugs/closed/shouldsucceed/1905.v |   2 +-
 test-suite/bugs/closed/shouldsucceed/2089.v |  17 +++
 test-suite/success/dependentind.v           |   3 +-
 theories/Classes/EquivDec.v                 |  15 +--
 theories/Classes/Equivalence.v              |   8 +-
 theories/Classes/Init.v                     |  11 +-
 theories/Classes/Morphisms.v                |  50 +++-----
 theories/Classes/Morphisms_Relations.v      |   1 +
 theories/Classes/RelationClasses.v          |   9 +-
 theories/Classes/SetoidAxioms.v             |   4 +-
 theories/Classes/SetoidClass.v              |   4 +-
 theories/Classes/SetoidTactics.v            |  12 +-
 theories/FSets/FMapFacts.v                  |   4 +-
 theories/FSets/FSetFacts.v                  |  10 +-
 theories/Logic/ConstructiveEpsilon.v        |   6 +-
 theories/Logic/FunctionalExtensionality.v   |   2 -
 theories/Program/Equality.v                 |  10 +-
 theories/Program/Wf.v                       |  12 +-
 theories/Setoids/Setoid.v                   |   4 +-
 tools/coq_makefile.ml4                      |  20 +--
 tools/coqdoc/cdglobals.ml                   |   3 +-
 tools/coqdoc/coqdoc.css                     |  33 +++++
 tools/coqdoc/coqdoc.sty                     |   3 +
 tools/coqdoc/main.ml                        |   7 +-
 tools/coqdoc/output.ml                      |  55 +++++---
 tools/coqdoc/output.mli                     |   5 +-
 tools/coqdoc/pretty.mll                     | 134 +++++++++++++------
 toplevel/classes.ml                         |  26 +++-
 toplevel/command.ml                         |  26 ++--
 toplevel/command.mli                        |   6 +-
 toplevel/himsg.ml                           |   6 +-
 toplevel/record.ml                          |   4 +-
 toplevel/vernacentries.ml                   |  17 +--
 toplevel/vernacexpr.ml                      |   4 +-
 122 files changed, 1127 insertions(+), 881 deletions(-)
 create mode 100644 doc/common/styles/html/simple/footer.html
 create mode 100644 doc/common/styles/html/simple/header.html
 create mode 100644 doc/common/styles/html/simple/style.css
 delete mode 100644 doc/stdlib/index-trailer.html
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2089.v

diff --git a/CHANGES b/CHANGES
index 494575fa..4bc0bd82 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,50 @@
+Changes from V8.2 to forthcoming V8.2pl1
+========================================
+
+Language and commands
+
+- Fixing Not_found bug in Theorem with.
+- Fixing pattern parsing bug #2087.
+- Fixing name aliases bug #2085 with modules.
+- Fixing checker bug #2065 with -impredicative-set option.
+- Complying with 8.1 heuristic when unification returns several solutions.
+- Add [Print Opaque Dependencies] command to print the assumptions and 
+  the opaque constants a definition uses.
+- Fixing performance issue in Program's type inference when there are
+  many existentials.
+- Fixing bug #2093, using Program does not require to import Program.Tactics
+  anymore, it will use [idtac] as the default obligation tactic.
+- Fix imports when requiring Setoid, to avoid cluttering the context with
+  internal names (possible source of incompatibility, import Morphisms to fix).
+- Fixing bug #2089, Combined Scheme was not treating parameters correctly.
+- Fixing Program to use hooks correctly, when called through [Program Coercion]
+  for example.
+- Fixing manual implicit arguments to always work and remove 
+  [Set Manual Implicit Arguments] option (possible source of incompatibility).
+- Fixing refine to work with typeclasses.
+- Fixing implementation of [Context] to discharge class instances only on definitions
+  using some of the parameters or the instance itself (possible source of 
+  incompatibility).
+
+Tactics
+
+- Fixing correct binding of quantified hypotheses for induction/destruction
+  when used in Ltac.
+- Fixing bad parentheses check in "pose (f binders := ...)" syntax.
+- Fixing unbalanced parenthesis in Ltac debug trace printer.
+- Fixing missing sort unification check in lemma application (bug #2084).
+- Fixing "as" clause of "apply in" that was not working in the general case.
+- Fixing eauto not using external hints with no pattern.
+
+Tools and development
+
+- Fixing missing -c option in coq_makefile.
+- Temporary hack for coqide.byte "double free or corruption" problem.
+- Added support for code development under Bazaar.
+- Added support for compilation under Solaris (thanks to Eric Le Lay, #2078).
+- Parsing fixes and support for parsing regular comments inline in coqdoc,
+  using option -parse-comments (suggestions by B. Pierce).
+
 Changes from V8.1 to V8.2
 =========================
 
diff --git a/COPYRIGHT b/COPYRIGHT
index 7ed31f15..8478bd4e 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -1,6 +1,6 @@
-The Coq proof assistant V7 and V8 includes software developed by the 
-Coq development team inside the LogiCal project, at INRIA, CNRS and
-University Paris Sud. 
+The Coq proof assistant V7 and V8 includes software developed by the
+Coq development team inside the TypiCal (formerly LogiCal) project, at
+INRIA, CNRS and University Paris Sud.
 
 Copyright 1999-2004 The Coq development team, 
 INRIA-CNRS, University Paris Sud, All rights reserved.
@@ -19,17 +19,9 @@ parsing/search.ml)
 	Pierre Courtieu, Lemme (contrib/funind)
 	Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
 	Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml)
+	Lionel Mamane, Radbout University, Nijmegen (additions to contrib/interface)
+	Cezary Kalyczyc, Radbout University, Nijmegen (additions to contrib/xml)
 
 The file CREDITS contains a list of past contributors
 The credits section in Reference Manual introduction details
 contributions.
-
-The Coq development Team (march 2004)
-	Bruno Barras (INRIA)
-	Pierre Corbineau (Université Paris Sud)
-	Jean-Christophe Filliâtre (CNRS)
-	Hugo Herbelin (INRIA)
-	Pierre Letouzey (Université Paris Sud)
-	Claude Marché (Université Paris Sud-INRIA)
-	Christine Paulin (Université Paris Sud)	
-	Clément Renard (INRIA)
diff --git a/CREDITS b/CREDITS
index b3d563ca..90dbd0b2 100644
--- a/CREDITS
+++ b/CREDITS
@@ -50,8 +50,6 @@ contrib/interface
   at Nijmegen, 2007-2008)
 contrib/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
-contrib/recdef
-  developed by Yves Bertot (INRIA-Marelle, 2005-2006)
 contrib/ring
   developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
   Loiseleur (LRI, 1997-1999)
@@ -80,16 +78,21 @@ theories/ZArith
   started by Pierre Crégut (France Telecom R&D, 1996)
 theories/IntMap
   developed by Jean Goubault-Larrecq (Dyade, 1998)
+theories/Numbers/Cyclic
+  developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry
+  (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and
+  Pierre Letouzey (PPS-Paris 7, 2008)
 theories/Strings
   developed by Laurent Théry (INRIA-Lemme, 2003)
 ide/utils
   some files come from Maxence Guesdon's Cameleon tool 
 
-Many discussions within the Démons team at LRI and the LogiCal project
-influenced significantly the design of Coq especially with
+Many discussions within the Démons team at LRI, and the
+LogiCal/TypiCal projects influenced significantly the design of
+components of Coq, especially with
 
-  J. Courant, P. Courtieu, J. Duprat, J. Goubault,
-  A. Miquel, C. Marché, B. Monate, B. Werner.
+  F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault,
+  A. Mahboubi, C. Marché, A. Miquel, B. Monate, P.-Y. Strub, B. Werner.
 
 Intensive users suggested improvements of the system : 
 
@@ -135,9 +138,11 @@ of the Coq Proof assistant during the indicated time :
                             LRI, 1997-now)
   Clément Renard (INRIA, 2001-2004)
   Claudio Sacerdoti Coen (INRIA, 2004-2005)
+  Amokrane Saïbi (INRIA, 1993-1998)
+  Vincent Siles (INRIA, 2007)
+  Élie Soubiran (INRIA, 2007-now)
   Matthieu Sozeau (INRIA, 2005-now)
   Arnaud Spiwack (INRIA, 2006-now)
-  Amokrane Saïbi (INRIA, 1993-1998)
   Benjamin Werner (INRIA, 1989-1994)
 
 ***************************************************************************
diff --git a/Makefile b/Makefile
index 70e9fb1f..6854de92 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
-# $Id: Makefile 11826 2009-01-22 06:43:35Z notin $ 
+# $Id: Makefile 12063 2009-04-08 15:38:39Z herbelin $ 
 
 
 # Makefile for Coq
@@ -24,14 +24,17 @@
 # by Emacs' next-error.
 ###########################################################################
 
+export SHELL:=/bin/bash
+
 export FIND_VCS_CLAUSE:='(' \
-  -name '{arch}' -or \
-  -name '.svn' -or \
-  -name '_darcs' -or \
-  -name '.git' -or \
-  -name 'debian' -or \
+  -name '{arch}' -o \
+  -name '.svn' -o \
+  -name '_darcs' -o \
+  -name '.git' -o \
+  -name '.bzr' -o \
+  -name 'debian' -o \
   -name "$${GIT_DIR}" \
-')' -prune -type f -or
+')' -prune -type f -o
 export PRUNE_CHECKER := -wholename ./checker/\* -prune -or
 
 FIND_PRINTF_P:=-print | sed 's|^\./||'
@@ -45,7 +48,7 @@ export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENVFILES:=theories/Numbers/Natural/BigN/NMake.v
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
 export MLFILES  := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml'  ')' $(FIND_PRINTF_P) | \
-  while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \
+  while read f; do if [ ! -e "$${f}4" ]; then echo "$$f"; fi; done) \
   $(GENMLFILES)
 export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
   $(GENMLIFILES)
@@ -152,15 +155,15 @@ clean: objclean cruftclean depclean docclean devdocclean
 objclean: archclean indepclean
 
 cruftclean: ml4clean
-	find . -name '*~' -or -name '*.annot' | xargs rm -f
+	find . -name '*~' -o -name '*.annot' | xargs rm -f
 	rm -f gmon.out core
 
 indepclean:
 	rm -f $(GENFILES)
 	rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
 	rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE)
-	find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f
-	find contrib test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
+	find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f
+	find contrib test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
 	rm -f */*.pp[iox] contrib/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
 	rm -f toplevel/mltop.byteml toplevel/mltop.optml
@@ -184,12 +187,13 @@ docclean:
 	rm -f doc/common/version.tex
 	rm -f doc/refman/*.eps doc/refman/Reference-Manual.html
 	rm -f doc/coq.tex
+	rm -f doc/refman/styles.hva doc/refman/cover.html 
 
 archclean: clean-ide cleantheories
 	rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN)
 	rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
 	rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE)
-	find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f
+	find . -name '*.cmx' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 	rm -f $(TOOLS) $(CSDPCERT)
 
 clean-ide:
@@ -214,7 +218,7 @@ distclean: clean cleanconfig
 
 cleantheories:
 	rm -f states/*.coq
-	find theories -name '*.vo' -or -name '*.glob' | xargs rm -f
+	find theories -name '*.vo' -o -name '*.glob' | xargs rm -f
 
 devdocclean:
 	find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \;
diff --git a/Makefile.build b/Makefile.build
index 19f13f15..703c5884 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -6,7 +6,7 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
-# $Id: Makefile.build 11935 2009-02-17 16:14:07Z notin $ 
+# $Id: Makefile.build 12169 2009-06-06 21:43:23Z herbelin $ 
 
 
 # Makefile for Coq
@@ -717,7 +717,7 @@ ifeq ($(BEST),opt)
 endif
 # csdpcert is not meant to be directly called by the user; we install
 # it with libraries
-	-$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega
+	-$(MKDIR) $(FULLCOQLIB)/contrib/micromega
 	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega
 	-$(INSTALLLIB) revision $(FULLCOQLIB)
 
@@ -960,7 +960,7 @@ else
 endif
 %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
 	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)( /bin/echo -n '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
+	$(HIDE)( printf "%s" '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 %.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml) %.ml4.d
diff --git a/Makefile.common b/Makefile.common
index 15faace0..d6f43cf5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -210,12 +210,11 @@ TACTICS:=\
   tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
   tactics/nbtermdn.cmo tactics/tacticals.cmo \
   tactics/hipattern.cmo tactics/tactics.cmo \
-  tactics/evar_tactics.cmo \
   tactics/hiddentac.cmo tactics/elim.cmo \
   tactics/dhyp.cmo tactics/auto.cmo \
   toplevel/ind_tables.cmo tactics/equality.cmo \
   tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \
-  tactics/tacinterp.cmo tactics/autorewrite.cmo \
+  tactics/tacinterp.cmo tactics/autorewrite.cmo tactics/evar_tactics.cmo \
   tactics/decl_interp.cmo tactics/decl_proof_instr.cmo
 
 TOPLEVEL:=\
diff --git a/Makefile.doc b/Makefile.doc
index aff812db..795e0e5c 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -125,7 +125,7 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
 	$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
 	(cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html)
 	$(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html
-	$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
+	-$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
 
 refman-quick:
 	(cd doc/refman;\
@@ -184,40 +184,32 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
 ### Standard library (browsable html format)
 
 ifeq ($(QUICK),1)
-doc/stdlib/index-body.html:
-	- rm -rf doc/stdlib/html
-	$(MKDIR) doc/stdlib/html
-	$(COQDOC) -q -d doc/stdlib/html --multi-index --html -g \
-	  -R theories Coq $(THEORIESVO:.vo=.v)
-	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
+doc/stdlib/html/genindex.html:
 else
-doc/stdlib/index-body.html: | $(COQDOC) $(THEORIESVO)
+doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO)
+endif
 	- rm -rf doc/stdlib/html
 	$(MKDIR) doc/stdlib/html
-	$(COQDOC) -q -d doc/stdlib/html --multi-index --html -g \
+	$(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
 	  -R theories Coq $(THEORIESVO:.vo=.v)
-	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
-endif
+	mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html
 
 doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
 	./doc/stdlib/make-library-index doc/stdlib/index-list.html
 
-doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html
-	cat doc/stdlib/index-list.html > $@
-	sed -n -e '/<table>/,/<\/table>/p' doc/stdlib/index-body.html >> $@
-	cat doc/stdlib/index-trailer.html >> $@
+doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html
+	cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@
+	cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@
 
 ### Standard library (light version, full version is definitely too big)
 
 ifeq ($(QUICK),1)
 doc/stdlib/Library.coqdoc.tex:
-	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
-            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
 else
 doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
+endif
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
             -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
-endif
 
 doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
 	(cd doc/stdlib;\
diff --git a/Makefile.stage1 b/Makefile.stage1
index a60d388f..c39a6372 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -6,6 +6,7 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
+export SHELL:=/bin/bash
 include Makefile.build
 
 # All includes must be declared secondary, otherwise make will delete
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 9e886837..f4ffb302 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -108,7 +108,7 @@ type compiled_library =
  
 open Validate
 let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
-let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_eng|]
+let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
 
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 14595fa5..0dc4a6a8 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq_config.mli 11858 2009-01-26 13:27:23Z notin $ i*)
+(*i $Id: coq_config.mli 12104 2009-04-24 18:10:10Z notin $ i*)
 
 val local : bool        (* local use (no installation) *)
 
@@ -45,4 +45,8 @@ val browser : string
 (** default web browser to use, may be overriden by environment
     variable COQREMOTEBROWSER *)
 
+val wwwcoq : string
+val wwwrefman : string
+val wwwstdlib : string
+
 val has_natdynlink : bool
diff --git a/configure b/configure
index c8508f52..1ba4eaba 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 ##################################
 #
@@ -6,8 +6,8 @@
 # 
 ##################################
 
-VERSION=8.2
-VOMAGIC=08200 
+VERSION=8.2pl1
+VOMAGIC=08200
 STATEMAGIC=58200
 DATE=`LANG=C date +"%B %Y"`
 
@@ -133,6 +133,7 @@ reals=all
 arch_spec=no
 coqide_spec=no
 browser_spec=no
+wwwcoq_spec=no
 with_geoproof=false
 with_doc=all
 with_doc_spec=no
@@ -216,6 +217,9 @@ while : ; do
     -browser|--browser) browser_spec=yes
 		      BROWSER=$2
 		      shift;;
+    -coqwebsite|--coqwebsite) wwwcoq_spec=yes
+                      WWWCOQ=$2
+                      shift;;
     -with-doc|--with-doc) with_doc_spec=yes
 		      case "$2" in
 			  yes|all) with_doc=all;;
@@ -285,7 +289,7 @@ case $arch_spec in
  	    ARCH=`/usr/bin/uname -s`
 	else
 	    echo "I can not automatically find the name of your architecture"
-	    echo -n\
+	    printf "%s"\
 		"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
 	    read ARCH
 	fi
@@ -358,6 +362,10 @@ if [ "$browser_spec" = "no" ]; then
     esac
 fi
 
+if [ "$wwwcoq_spec" = "no" ]; then
+    WWWCOQ="http://www.lix.polytechnique.fr/coq/"
+fi
+
 #########################################
 # Objective Caml programs
 
@@ -853,6 +861,7 @@ echo "  Documentation                     : None"
 fi
 echo "  CoqIde                            : $COQIDE"
 echo "  Web browser                       : $BROWSER"
+echo "  Coq web site                      : $WWWCOQ"
 echo ""
 
 echo "  Paths for true installation:"
@@ -944,6 +953,9 @@ let state_magic_number = $STATEMAGIC
 let exec_extension = "$EXE"
 let with_geoproof = ref $with_geoproof
 let browser = "$ESCBROWSER"
+let wwwcoq = "$WWWCOQ"
+let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
+let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
 
 END_OF_COQ_CONFIG
 
@@ -1068,4 +1080,4 @@ echo
 echo "*Warning* To compile the system for a new architecture"
 echo "          don't forget to do a 'make archclean' before './configure'."
 
-# $Id: configure 11934 2009-02-17 15:58:54Z notin $
+# $Id: configure 12219 2009-07-01 09:58:00Z notin $
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index e59de34a..e0f43193 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -58,8 +58,8 @@ let explore_tree pfs =
     | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
     | Intro identifier -> "Intro"
     | Cut (bool, _, identifier, types) -> "Cut"
-    | FixRule (identifier, int, l) -> "FixRule"
-    | Cofix (identifier, l) -> "Cofix"
+    | FixRule (identifier, int, l, _) -> "FixRule"
+    | Cofix (identifier, l, _) -> "Cofix"
     | Convert_concl (types, cast_kind) -> "Convert_concl"
     | Convert_hyp named_declaration -> "Convert_hyp"
     | Thin identifier_list -> "Thin"
@@ -411,8 +411,8 @@ and depends_of_prim_rule pr acc = match pr with
   | Refine c                     -> depends_of_constr c acc
   | Intro id                     -> acc
   | Cut (_, _, _, t)             -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
-  | FixRule (_, _, l)            -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
-  | Cofix (_, l)                 -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
+  | FixRule (_, _, l, _)         -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
+  | Cofix (_, l, _)              -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
   | Convert_concl (t, _)         -> depends_of_constr t acc
   | Convert_hyp (_, None, t)     -> depends_of_constr t acc
   | Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc)
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index ba00fce5..c0b64379 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: subtac.ml 12194 2009-06-17 16:38:09Z msozeau $ *)
 
 open Global
 open Pp
@@ -99,7 +99,7 @@ let declare_assumption env isevars idl is_coe k bl c nl =
       Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None 
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl
+      List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
@@ -127,7 +127,6 @@ let check_fresh (loc,id) =
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
-  check_required_library ["Coq";"Program";"Tactics"];
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
@@ -143,7 +142,7 @@ let subtac (loc, command) =
 	  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) 
 	    (fun _ _ -> ())
       | DefineBody (bl, _, c, tycon) -> 
-	  ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon))
+	  ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
   | VernacFixpoint (l, b) -> 
       List.iter (fun ((lid, _, _, _, _), _) -> 
 	check_fresh lid;
@@ -237,9 +236,6 @@ let subtac (loc, command) =
 	  debug 2 (Himsg.explain_pretype_error env exn);
 	  raise e
 
-      | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
-	  raise e)
+      | e'' -> raise e)
 	
-  | e -> 
-      msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
-      raise e
+  | e -> raise e
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 1d213db9..bd06407f 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: subtac_cases.ml 12194 2009-06-17 16:38:09Z msozeau $ *)
 
 open Cases
 open Util
@@ -301,8 +301,8 @@ module Cases_F(Coercion : Coercion.S) : S = struct
 
 let inh_coerce_to_ind isevars env ty tyi =
   let expected_typ = inductive_template isevars env None tyi in
-     (* devrait être indifférent d'exiger leq ou pas puisque pour 
-        un inductif cela doit être égal *)
+     (* devrait être indifférent d'exiger leq ou pas puisque pour 
+        un inductif cela doit être égal *)
   let _ = e_cumul env isevars expected_typ ty in ()
 
 let unify_tomatch_with_patterns isevars env loc typ pats =
@@ -696,9 +696,9 @@ let insert_aliases_eqn sign eqnnames alias_rest eqn =
 	    
 
 let insert_aliases env sigma alias eqns =
-  (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
-  (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
-  (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
+  (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
+  (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
+  (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
   let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
   let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
   (* names2 takes the meet of all needed aliases *)
@@ -843,7 +843,7 @@ let infer_predicate loc env isevars typs cstrs indf =
       (* Non dependent case -> turn it into a (dummy) dependent one *)
       let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
-      (true,pred) (* true = dependent -- par défaut *)
+      (true,pred) (* true = dependent -- par défaut *)
     else
 (*
       let s = get_sort_of env (evars_of isevars) typs.(0) in
@@ -1294,7 +1294,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
   List.fold_left mkSpecialLetInJudge j sign
 
 (* pour les alias des initiaux, enrichir les env de ce qu'il faut et
-substituer après par les initiaux *)
+substituer après par les initiaux *)
 
 (**************************************************************************)
 (* Preparation of the pattern-matching problem                            *)
@@ -1319,99 +1319,6 @@ let matx_of_eqns env eqns =
 (************************************************************************)
 (* preparing the elimination predicate if any                          *)
 
-let build_expected_arity env isevars isdep tomatchl =
-  let cook n = function
-    | _,IsInd (_,IndType(indf,_)) ->
-        let indf' = lift_inductive_family n indf in
-	Some (build_dependent_inductive env indf', fst (get_arity env indf'))
-    | _,NotInd _ -> None
-  in
-  let rec buildrec n env = function
-    | [] -> new_Type ()
-    | tm::ltm ->
-	match cook n tm with
-	  | None -> buildrec n env ltm
-	  | Some (ty1,aritysign) ->
-	      let rec follow n env = function
-		| d::sign ->
-		    mkProd_or_LetIn_name env
-		      (follow (n+1) (push_rel d env) sign) d
-		| [] ->
-		    if isdep then
-		      mkProd (Anonymous, ty1, 
-			      buildrec (n+1)
-				(push_rel_assum (Anonymous, ty1) env)
-				ltm)
-		    else buildrec n env ltm
-	      in follow n env (List.rev aritysign)
-  in buildrec 0 env tomatchl
-
-let extract_predicate_conclusion isdep tomatchl pred =
-  let cook = function
-    | _,IsInd (_,IndType(_,args)) -> Some (List.length args)
-    | _,NotInd _ -> None in
-  let rec decomp_lam_force n l p =
-    if n=0 then (l,p) else
-    match kind_of_term p with
-      | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
-      | _ -> (* eta-expansion *)
-          let na = Name (id_of_string "x") in
-          decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
-  let rec buildrec allnames p = function
-    | [] -> (List.rev allnames,p)
-    | tm::ltm ->
-	match cook tm with
-	  | None -> 
-              let p = 
-                (* adjust to a sign containing the NotInd's *)
-                if isdep then lift 1 p else p in
-              let names = if isdep then [Anonymous] else [] in
-              buildrec (names::allnames) p ltm
-	  | Some n ->
-              let n = if isdep then n+1 else n in
-              let names,p = decomp_lam_force n [] p in
-              buildrec (names::allnames) p ltm
-  in buildrec [] pred tomatchl
-
-let set_arity_signature dep n arsign tomatchl pred x =
-  (* avoid is not exhaustive ! *)
-  let rec decomp_lam_force n avoid l p =
-    if n = 0 then (List.rev l,p,avoid) else
-    match p with
-      | RLambda (_,(Name id as na),k,_,c) -> 
-          decomp_lam_force (n-1) (id::avoid) (na::l) c
-      | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
-      | _ ->
-          let x = next_ident_away (id_of_string "x") avoid in
-          decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-          (* eta-expansion *)
-            (let a = RVar (dummy_loc,x) in
-             match p with
-               | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-               | _ -> (RApp (dummy_loc,p,[a]))) in
-  let rec decomp_block avoid p = function
-    | ([], _) -> x := Some p
-    | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l')  ->
-	let (ind,params) = dest_ind_family indf in
-        let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p 
-        in
-        let na,p,avoid' = 
-          if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
-        in 
-        y :=
-        (List.hd na,
-         if List.for_all ((=) Anonymous) nal then
-           None
-         else
-           Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
-        decomp_block avoid' p (l,l')
-    | (_::l),(y::l') ->
-        y := (Anonymous,None);
-        decomp_block avoid p (l,l')
-    | _ -> anomaly "set_arity_signature"
-  in
-  decomp_block [] pred (tomatchl,arsign)
-
 let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
@@ -1569,9 +1476,6 @@ let eq_id avoid id =
 
 let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
 let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = 
-  mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
     
 let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
 
@@ -1828,24 +1732,6 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 
  * A type constraint but no annotation case: it is assumed non dependent.
  *)
-
-let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
-  (* We extract the signature of the arity *)
-  let arsign = extract_arity_signature env tomatchs sign in
-  let env = List.fold_right push_rels arsign env in
-  let allnames = List.rev (List.map (List.map pi1) arsign) in
-    match rtntyp with
-      | Some rtntyp ->
-	  let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
-	  let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
-	    Some (build_initial_predicate true allnames predccl)
-      | None -> 
-	  match valcon_of_tycon tycon with
-	    | Some ty -> 
-		let names,pred = 
-		  oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty
-		in Some (build_initial_predicate true names pred)
-	    | None -> None
   
 let lift_ctx n ctx = 
   let ctx', _ =
@@ -1862,7 +1748,7 @@ let abstract_tomatch env tomatchs =
 	     Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names
 	   | _ -> 
 	       let name = next_ident_away_from (id_of_string "filtered_var") names in
-		 (mkRel 1, lift_tomatch_type 1 t) :: lift_ctx 1 prev, 
+		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, 
 	       (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, 
 	       name :: names)
       ([], [], []) tomatchs
@@ -1912,7 +1798,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 		      let previd, id = 
 			let name = 
 			  match kind_of_term arg with 
-			      Rel n -> pi1 (lookup_rel n (rel_context env))
+			      Rel n -> pi1 (Environ.lookup_rel n env)
 			    | _ -> name
 			in
 			  make_prime avoid name 
@@ -2025,6 +1911,25 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
 	ignore(Typing.sort_of env' evm pred); pred
     with _ -> lift nar c
 
+
+let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
+  (* We extract the signature of the arity *)
+  let arsign = extract_arity_signature env tomatchs sign in
+  let newenv = List.fold_right push_rels arsign env in
+  let allnames = List.rev (List.map (List.map pi1) arsign) in
+    match rtntyp with
+      | Some rtntyp ->
+	  let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
+	  let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
+	    Some (build_initial_predicate true allnames predccl)
+      | None -> 
+	  match valcon_of_tycon tycon with
+	    | Some ty -> 
+		let pred = 
+		  prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) tomatchs arsign ty
+		in Some (build_initial_predicate true allnames pred)
+	    | None -> None
+
 let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
 
   let typing_fun tycon env = typing_fun tycon env isevars in
@@ -2103,26 +2008,25 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
       (* with the type of arguments to match *)
       let tmsign = List.map snd tomatchl in
       let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in
-	
-	  (* We push the initial terms to match and push their alias to rhs' envs *)
-	  (* names of aliases will be recovered from patterns (hence Anonymous here) *)
-	  let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-	    
-	  let pb =
-	    { env      = env;
-	      isevars  = isevars;
-	      pred     = pred;
-	      tomatch  = initial_pushed;
-	      history  = start_history (List.length initial_pushed);
-	      mat      = matx;
-	      caseloc  = loc;
-	      casestyle= style;
-	      typing_function = typing_fun } in
-	    
-	  let j = compile pb in
-	  (* We check for unused patterns *)
-	  List.iter (check_unused_pattern env) matx;
-	    inh_conv_coerce_to_tycon loc env isevars j tycon	  
 
+      (* We push the initial terms to match and push their alias to rhs' envs *)
+      (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+      let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+      let pb =
+	{ env      = env;
+	  isevars  = isevars;
+	  pred     = pred;
+	  tomatch  = initial_pushed;
+	  history  = start_history (List.length initial_pushed);
+	  mat      = matx;
+	  caseloc  = loc;
+	  casestyle= style;
+	  typing_function = typing_fun } in
+	
+      let j = compile pb in
+	(* We check for unused patterns *)
+	List.iter (check_unused_pattern env) matx;
+	inh_conv_coerce_to_tycon loc env isevars j tycon	  
+	  
 end
   
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 0d44a0c0..9b692d85 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: subtac_classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 open Pretyping
 open Evd
@@ -182,7 +182,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   in
     isevars := undefined_evars !isevars;
     Evarutil.check_evars env Evd.empty !isevars termtype;
-    let hook gr = 
+    let hook vis gr = 
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
       let inst = Typeclasses.new_instance k pri global cst in
 	Impargs.declare_manual_implicits false gr ~enriching:false imps;
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 4876b065..c8c7ff72 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -390,7 +390,7 @@ let interp_recursive fixkind l boxed =
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs = 
-    States.with_heavy_rollback (fun () -> 
+    States.with_state_protection (fun () -> 
       List.iter (Command.declare_interning_data impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d2e831ef..3dcd43d2 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -17,8 +17,6 @@ open Evd
 open Declare
 open Proof_type
 
-type definition_hook = global_reference -> unit
-
 let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
@@ -56,14 +54,14 @@ type program_info = {
   prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
   prg_notations : notations ;
   prg_kind : definition_kind;
-  prg_hook : definition_hook;
+  prg_hook : Tacexpr.declaration_hook;
 }
 
 let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
 let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
-let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
+let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId [])
 
 let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
@@ -203,7 +201,7 @@ let declare_definition prg =
 	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
 	    Impargs.declare_manual_implicits false gr prg.prg_implicits;
 	  print_message (Subtac_utils.definition_message prg.prg_name);
-	  prg.prg_hook gr;
+	  prg.prg_hook local gr;
 	  gr
 
 open Pp
@@ -234,6 +232,7 @@ let reduce_fix =
 
 let declare_mutual_definition l =
   let len = List.length l in
+  let first = List.hd l in
   let fixdefs, fixtypes, fiximps = 
     list_split3
       (List.map (fun x -> 
@@ -241,11 +240,11 @@ let declare_mutual_definition l =
 	  snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixkind = Option.get (List.hd l).prg_fixkind in
+  let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let boxed = true (* TODO *) in
-  let fixnames = (List.hd l).prg_deps in
+  let (local,boxed,kind) = first.prg_kind in
+  let fixnames = first.prg_deps in
   let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
   let indexes, fixdecls =
     match fixkind with
@@ -260,9 +259,11 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
-    List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations;
+    List.iter (Command.declare_interning_data ([],[])) first.prg_notations;
     Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
-    (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
+    let gr = List.hd kns in
+    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
+      first.prg_hook local gr; kn
       
 let declare_obligation obl body =
   match obl.obl_status with
@@ -525,7 +526,7 @@ let show_term n =
 	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls =
+let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n b t [] None [] obls implicits kind hook in
   let obls,_ = prg.prg_obligations in
@@ -543,11 +544,11 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 	
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, imps, obls) ->
-	let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun x -> ()) in
+	let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in
 	  ProgMap.add n prg acc)
       !from_prg l
   in
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 60c0a413..766af2fa 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -21,13 +21,11 @@ val default_tactic : unit -> Proof_type.tactic
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool
 
-type definition_hook = global_reference -> unit
-
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
-  ?hook:definition_hook -> obligation_info -> progress
+  ?hook:Tacexpr.declaration_hook -> obligation_info -> progress
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
 
@@ -36,6 +34,7 @@ val add_mutual_definitions :
       (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> 
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
+  ?hook:Tacexpr.declaration_hook -> 
   notations ->
   Command.fixpoint_kind -> unit
 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 07a75720..3ae7c95d 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping.ml 11574 2008-11-10 13:45:05Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Global
 open Pp
@@ -84,13 +84,6 @@ let find_with_index x l =
     | [] -> raise Not_found
   in aux 0 l
 
-let list_split_at index l = 
-  let rec aux i acc = function
-      hd :: tl when i = index -> (List.rev acc), tl
-    | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_at: Invalid argument"
-  in aux 0 [] l
-
 open Vernacexpr
 
 let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
@@ -136,9 +129,9 @@ let subtac_process env isevars id bl c tycon =
 
 open Subtac_obligations
 
-let subtac_proof kind env isevars id bl c tycon =
+let subtac_proof kind hook env isevars id bl c tycon =
   let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
   let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
   let evm' = Subtac_utils.evars_of_term evm evm' coqt in
   let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
-    add_definition id def ty ~implicits:imps ~kind:kind evars
+    add_definition id def ty ~implicits:imps ~kind ~hook evars
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index 1d8eb250..ba0b7cd2 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -19,5 +19,6 @@ val interp :
 val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
 
-val subtac_proof : Decl_kinds.definition_kind -> env -> evar_defs ref -> identifier -> local_binder list ->
+val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> 
+  env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index cdbc4023..2ee2018e 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -64,15 +64,17 @@ let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
 let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
 let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
 
-let jmeq_ind =   
-  lazy (check_required_library ["Coq";"Logic";"JMeq"]; 
-	init_constant ["Logic";"JMeq"] "JMeq")
-let jmeq_rec = 
-  lazy (check_required_library ["Coq";"Logic";"JMeq"]; 
-	init_constant ["Logic";"JMeq"] "JMeq_rec")
-let jmeq_refl = 
-  lazy (check_required_library ["Coq";"Logic";"JMeq"];
-	init_constant ["Logic";"JMeq"] "JMeq_refl")
+let jmeq_ind () =   
+  check_required_library ["Coq";"Logic";"JMeq"]; 
+  init_constant ["Logic";"JMeq"] "JMeq"
+
+let jmeq_rec () = 
+  check_required_library ["Coq";"Logic";"JMeq"]; 
+  init_constant ["Logic";"JMeq"] "JMeq_rec"
+
+let jmeq_refl () = 
+  check_required_library ["Coq";"Logic";"JMeq"];
+  init_constant ["Logic";"JMeq"] "JMeq_refl"
 
 let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
 let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
@@ -277,8 +279,8 @@ let mkSubset name typ prop =
 
 let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
 let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (jmeq_ind (), [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (jmeq_refl (), [| typ; x |])
 
 let unsafe_fold_right f = function
     hd :: tl -> List.fold_right f tl hd
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 964f668f..9c014286 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -45,9 +45,9 @@ val and_typ : constr lazy_t
 val eqdep_ind : constr lazy_t
 val eqdep_rec : constr lazy_t
 
-val jmeq_ind : constr lazy_t
-val jmeq_rec : constr lazy_t
-val jmeq_refl : constr lazy_t
+val jmeq_ind : unit -> constr
+val jmeq_rec : unit -> constr
+val jmeq_refl : unit -> constr
 
 val boolind : constr lazy_t
 val sumboolind : constr lazy_t
@@ -103,7 +103,7 @@ val mk_ex_pi1 : constr -> constr -> constr -> constr
 val mk_ex_pi1 : constr -> constr -> constr -> constr
 val mk_eq : types -> constr -> constr -> types
 val mk_eq_refl : types -> constr -> constr
-val mk_JMeq : types -> constr-> types -> constr -> types
+val mk_JMeq : types -> constr -> types -> constr -> types
 val mk_JMeq_refl : types -> constr -> constr
 val mk_conj : types list -> types
 val mk_not : types -> types
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index a501fb6a..7503d632 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -82,8 +82,8 @@ let first_word s =
 let string_of_prim_rule x = match x with
   | Proof_type.Intro _-> "Intro"
   | Proof_type.Cut _ -> "Cut"
-  | Proof_type.FixRule (_,_,_) -> "FixRule"
-  | Proof_type.Cofix (_,_)-> "Cofix"
+  | Proof_type.FixRule _ -> "FixRule"
+  | Proof_type.Cofix _ -> "Cofix"
   | Proof_type.Refine _ -> "Refine"
   | Proof_type.Convert_concl _ -> "Convert_concl"
   | Proof_type.Convert_hyp _->"Convert_hyp"
diff --git a/dev/base_include b/dev/base_include
index d4366843..711dcb2a 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -14,6 +14,9 @@
 #directory "tactics";;
 #directory "translate";;
 
+#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
+#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
+
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
@@ -112,6 +115,9 @@ open Proof_type
 open Redexpr
 open Refiner
 open Tacmach
+open Decl_proof_instr
+open Tactic_debug
+open Decl_mode
 
 open Auto
 open Autorewrite
diff --git a/doc/common/styles/html/simple/footer.html b/doc/common/styles/html/simple/footer.html
new file mode 100644
index 00000000..308b1d01
--- /dev/null
+++ b/doc/common/styles/html/simple/footer.html
@@ -0,0 +1,2 @@
+</body>
+</html>
diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html
new file mode 100644
index 00000000..14d2f988
--- /dev/null
+++ b/doc/common/styles/html/simple/header.html
@@ -0,0 +1,13 @@
+<!DOCTYPE html 
+     PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+
+<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
+<link rel="stylesheet" href="coqdoc.css" type="text/css"/>
+<title>The Coq Standard Library</title>
+</head>
+
+<body>
+
diff --git a/doc/common/styles/html/simple/style.css b/doc/common/styles/html/simple/style.css
new file mode 100644
index 00000000..0b1e640b
--- /dev/null
+++ b/doc/common/styles/html/simple/style.css
@@ -0,0 +1,13 @@
+#footer {
+    border-top: solid black 1pt;
+    text-align: center;
+    text-indent: 0pt;
+}
+
+.menu { }
+.menu li {
+    display: inline;
+    margin: 0pt;
+    padding: .5ex 1em;
+    list-style: none 
+}
\ No newline at end of file
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0ab4e47b..484002c3 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -1,17 +1,5 @@
-<!DOCTYPE html 
-     PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
-    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
 
-<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
-<head>
-<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
-<link rel="stylesheet" href="css/context.css" type="text/css"/>
-<title>The Coq Standard Library</title>
-</head>
-
-<body>
-
-<H1>The Coq Standard Library</H1>
+<h1>The Coq Standard Library</h1>
 
 <p>Here is a short description of the Coq standard library, which is
 distributed with the system.
@@ -323,8 +311,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
 
   <dd> 
     theories/Setoids/Setoid.v
-    theories/Setoids/Setoid_tac.v
-    theories/Setoids/Setoid_Prop.v
   </dd>
     
   <dt> <b>Lists</b>:
diff --git a/doc/stdlib/index-trailer.html b/doc/stdlib/index-trailer.html
deleted file mode 100644
index 308b1d01..00000000
--- a/doc/stdlib/index-trailer.html
+++ /dev/null
@@ -1,2 +0,0 @@
-</body>
-</html>
diff --git a/ide/coq.ml b/ide/coq.ml
index e2649c82..a44428c7 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 11826 2009-01-22 06:43:35Z notin $ *)
+(* $Id: coq.ml 11948 2009-02-27 16:01:53Z glondu $ *)
 
 open Vernac
 open Vernacexpr
@@ -424,6 +424,8 @@ let interp_with_options verbosely options s =
   prerr_endline s;
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
+  (* Temporary hack to make coqide.byte work (WTF???) *)
+  Pervasives.prerr_endline "";
   match pe with 
     | None -> assert false
     | Some((loc,vernac) as last) ->
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ea2dfe4d..cc147d5e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml 11853 2009-01-23 18:40:58Z notin $ *)
+(* $Id: coqide.ml 12104 2009-04-24 18:10:10Z notin $ *)
 
 open Preferences
 open Vernacexpr
@@ -3237,7 +3237,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					    ~callback:
 					    (fun () -> 
 					       let av = Option.get ((get_current_view ()).analyzed_view) in 
-						 browse av#insert_message (!current.doc_url ^ "main.html")) in
+						 browse av#insert_message (!current.doc_url)) in
 					  let _ = help_factory#add_item "Browse Coq _Library" 
 					    ~callback:
 					    (fun () -> 
@@ -3518,8 +3518,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 							    let about_full_string =
 							      "\nCoq is developed by the Coq Development Team\
        \n(INRIA - CNRS - University Paris 11 and partners)\
-       \nWeb site: http://coq.inria.fr\
-       \nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
+       \nWeb site: " ^ Coq_config.wwwcoq ^
+       "\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
        \n\
        \nCredits for CoqIDE, the Integrated Development Environment for Coq:\
        \n\
diff --git a/ide/preferences.ml b/ide/preferences.ml
index dba56a77..ffb346d9 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: preferences.ml 11276 2008-07-28 00:28:34Z glondu $ *)
+(* $Id: preferences.ml 12104 2009-04-24 18:10:10Z notin $ *)
 
 open Configwin
 open Printf
@@ -135,8 +135,8 @@ let (current:pref ref) =
 (*    text_font = Pango.Font.from_string "sans 12";*)
     text_font = Pango.Font.from_string "Monospace 10";
 
-    doc_url = "http://coq.inria.fr/doc/";
-    library_url = "http://coq.inria.fr/library/";
+    doc_url = Coq_config.wwwrefman;
+    library_url = Coq_config.wwwstdlib;
     
     show_toolbar = true;
     contextual_menus_on_goal = true;
diff --git a/install.sh b/install.sh
index 277222f5..c2f8215b 100755
--- a/install.sh
+++ b/install.sh
@@ -1,4 +1,4 @@
-#! /bin/sh
+#! /bin/bash
 
 dest="$1"
 shift
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 86e02623..cd4efe27 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: environ.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: environ.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Util
 open Names
@@ -554,7 +554,7 @@ fun env field value ->
 type context_object =
   | Variable of identifier (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
-
+  | Opaque of constant     (* An opaque constant. *)
 
 (* Defines a set of [assumption] *)
 module OrderedContextObject = 
@@ -566,15 +566,19 @@ struct
       | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2
 	          (* spiwack: it would probably be cleaner
 		     to provide a [kn_ord] function *)
+      | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2
       | Variable _ , Axiom _ -> -1
       | Axiom _ , Variable _ -> 1
+      | Opaque _ , _ -> -1
+      | _, Opaque _ -> 1
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
 
-let assumptions (* t env *) =   
+let assumptions ?(add_opaque=false) st (* t env *) =
+  let (idts,knst) = st in
   (* Infix definition for chaining function that accumulate
      on a and a ContextObjectSet, ContextObjectMap.  *)
   let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
@@ -650,16 +654,26 @@ let assumptions (* t env *) =
 
   and add_kn kn env s acc =
     let cb = lookup_constant kn env in
-    match cb.Declarations.const_body with
-    | None -> 
-	let ctype = 
-	  match cb.Declarations.const_type with
-	  | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
-	  | NonPolymorphicType t -> t
-	in
-	(s,ContextObjectMap.add (Axiom kn) ctype acc)
-    | Some body -> aux (Declarations.force body) env s acc
-
+    let do_type cst =
+      let ctype =
+	match cb.Declarations.const_type with
+	| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+	| NonPolymorphicType t -> t
+      in
+	(s,ContextObjectMap.add cst ctype acc)
+    in
+    let (s,acc) =
+      if cb.Declarations.const_body <> None
+	&& (cb.Declarations.const_opaque || not (Cpred.mem kn knst))
+	&& add_opaque 
+      then
+	do_type (Opaque kn)
+      else (s,acc)
+    in
+      match cb.Declarations.const_body with
+      | None -> do_type (Axiom kn)
+      | Some body -> aux (Declarations.force body) env s acc
+	  
   and aux_memoize_kn kn env =
     try_and_go (Axiom kn) (add_kn kn env)
  in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 97e19782..b68123f6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: environ.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: environ.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -244,13 +244,14 @@ val register : env -> field -> Retroknowledge.entry -> env
 type context_object =
   | Variable of identifier (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
+  | Opaque of constant     (* An opaque constant. *)
 
 (* AssumptionSet.t is a set of [assumption] *)
 module OrderedContextObject :  Set.OrderedType with type t = context_object
 module ContextObjectMap : Map.S with type key = context_object
 
-(* collects all the assumptions on which a term relies (together with
-   their type *)
-val assumptions : constr -> env -> Term.types ContextObjectMap.t
+(* collects all the assumptions (optionally including opaque definitions) 
+   on which a term relies (together with their type) *)
+val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t
 
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ab4b8e47..9a76922b 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mod_subst.ml 10849 2008-04-25 15:55:16Z soubiran $ *)
+(* $Id: mod_subst.ml 11924 2009-02-13 13:51:54Z soubiran $ *)
 
 open Pp
 open Util
@@ -250,11 +250,11 @@ let join (subst1 : substitution) (subst2 : substitution) =
       try
 	let res =
 	  match resolve with
-              Some res -> res
-	    | None ->
+	    |None -> begin
 		match resolve' with
 		    None -> raise BothSubstitutionsAreIdentitySubstitutions
-		  | Some res -> raise (ChangeDomain res)
+		  | Some res -> raise (ChangeDomain res) end
+	    | Some res -> res
 	in
 	  Some
 	    (List.map
@@ -356,23 +356,23 @@ let update_subst subst1 subst2 =
 	| MPI mp -> mp
     in
    match mp with 
-     | MPbound mbid ->  ((MBI mbid),newmp)::l
-     | MPself msid ->  ((MSI msid),newmp)::l
-     | _ ->   ((MPI mp),newmp)::l
+     | MPbound mbid ->  ((MBI mbid),newmp,resolve)::l
+     | MPself msid ->  ((MSI msid),newmp,resolve)::l
+     | _ ->   ((MPI mp),newmp,resolve)::l
   in 
   let subst_mbi = Umap.fold subst_inv subst2 [] in
   let alias_subst key (mp,resolve) sub=
     let newsetkey = 
       match key with
 	| MPI mp1 -> 
-	    let compute_set_newkey l (k,mp') = 
+	    let compute_set_newkey l (k,mp',resolve) = 
 	      let mp_from_key = match k with
 		  	| MBI msid -> MPbound msid
 			| MSI msid -> MPself msid
 			| MPI mp -> mp
 	      in
 	      let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
-		if new_mp1 == mp1 then l else (MPI new_mp1)::l
+		if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l
 	    in
 	    begin
 	      match List.fold_left compute_set_newkey [] subst_mbi with
@@ -384,7 +384,7 @@ let update_subst subst1 subst2 =
       match newsetkey with
 	| None -> sub
 	| Some l -> 
-	    List.fold_left (fun s k -> Umap.add k (mp,resolve) s)
+	    List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s)
 	      sub l
   in
     Umap.fold alias_subst subst1 empty_subst
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 25a11c69..949a7402 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 11514 2008-10-28 13:39:02Z soubiran $ i*)
+(*i $Id: modops.ml 11923 2009-02-13 12:20:27Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -272,9 +272,9 @@ let rec eval_struct env = function
 	      (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-      let sub_alias1 = update_subst sub_alias 
-	(map_mbid farg_id mp (None)) in
-      let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in
+    let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in  
+    let sub_alias1 = update_subst sub_alias 
+	(map_mbid farg_id mp (Some resolve)) in
 	eval_struct env (subst_struct_expr 
 			   (join sub_alias1 
 			      (map_mbid farg_id mp (Some resolve))) fbody_b)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fbb05a2d..7a2db86b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 11453 2008-10-15 14:42:34Z soubiran $ *)
+(* $Id: safe_typing.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Util
 open Names
@@ -113,7 +113,7 @@ let add_constraints cst senv =
 (* terms which are closed under the environnement env, i.e
    terms which only depends on constant who are themselves closed *)
 let closed env term = 
-  ContextObjectMap.is_empty (assumptions env term)
+  ContextObjectMap.is_empty (assumptions full_transparent_state env term)
 
 (* the set of safe terms in an environement any recursive set of
    terms who are known not to prove inconsistent statement. It should
diff --git a/lib/util.ml b/lib/util.ml
index a8a99c0b..dce36419 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: util.ml 12181 2009-06-10 20:53:09Z glondu $ *)
 
 open Pp
 
@@ -257,7 +257,7 @@ let classify_unicode unicode =
     (* utf-8 arrows and brackets U27E0-U27FF *)
     | x when 0x27E0 <= x & x <= 0x27FF -> UnicodeSymbol
     (* utf-8 brackets, braces and parentheses *)
-    | x when 0x2980 <= x & x <= 0x299F -> UnicodeSymbol
+    | x when 0x2980 <= x & x <= 0x29FF -> UnicodeSymbol
     (* utf-8 miscellaneous including double-plus U29F0-U29FF *)
     | x when 0x29F0 <= x & x <= 0x29FF -> UnicodeSymbol
     | _ -> raise UnsupportedUtf8
diff --git a/library/declare.ml b/library/declare.ml
index 4bdc11c3..c349bef1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: declare.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** This module is about the low-level declaration of logical objects *)
 
@@ -43,7 +43,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
+  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
@@ -58,7 +58,7 @@ let cache_variable ((sp,_),o) =
     | SectionLocalAssum (ty, impl, keep) ->
         let cst = Global.push_named_assum (id,ty) in
 	let impl = if impl then Lib.Implicit else Lib.Explicit in
-	let keep = if keep then Some ty else None in
+	let keep = if keep <> [] then Some (ty, keep) else None in
 	impl, true, cst, keep
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
diff --git a/library/declare.mli b/library/declare.mli
index 78d3f027..2f1cd06e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declare.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: declare.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -34,7 +34,7 @@ open Nametab
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
+  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3026143b..93021384 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 11898 2009-02-10 10:52:45Z soubiran $ i*)
+(*i $Id: declaremods.ml 12204 2009-06-22 16:06:49Z soubiran $ i*)
 open Pp
 open Util
 open Names
@@ -642,29 +642,30 @@ let rec get_modtype_substobjs env = function
 	    (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-    let sub3=
+      let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
+      let mbid,mbids= (match mbids with
+	   | mbid::mbids -> mbid,mbids
+	   | [] -> match mexpr with
+	       | MSEident _  -> error "Application of a non-functor"
+	       | _ -> error "Application of a functor with too few arguments") in
+      let resolve =
+	Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
+      let sub3=
 	if sub1 = empty_subst then
-	  update_subst sub_alias (map_mbid farg_id mp None)
+	  update_subst sub_alias (map_mbid farg_id mp (Some resolve))
 	else
-	  let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+	  let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
 	  let sub_alias' =  update_subst sub_alias sub1' in
 	    join sub1' sub_alias'
       in
-      let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
-       let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
-	(match mbids with
-	   | mbid::mbids ->
-               let resolve =
-		 Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
-		 (* application outside the kernel, only for substitutive
-                    objects (that are all non-logical objects) *)
-		((join 
-		    (join subst sub3)
-		    (map_mbid mbid mp (Some resolve)))
-		       , mbids, msid, objs)
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments")
+      let sub3 = join sub3 
+	(update_subst sub_alias (map_mbid farg_id mp (Some resolve))) in
+	(* application outside the kernel, only for substitutive
+           objects (that are all non-logical objects) *)
+	((join 
+	    (join subst sub3)
+	    (map_mbid mbid mp (Some resolve)))
+	   , mbids, msid, objs)
   | MSEapply (_,mexpr) ->
       Modops.error_application_to_not_path mexpr
 
@@ -948,30 +949,32 @@ let rec get_module_substobjs env = function
 	    (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-
+      let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
+      let mbid,mbids = 
+	(match mbids with
+	   | mbid::mbids ->mbid,mbids
+	       
+	   | [] -> match mexpr with
+	       | MSEident _  -> error "Application of a non-functor"
+	       | _ -> error "Application of a functor with too few arguments") in
+      let resolve =
+	Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
       let sub3=
 	if sub1 = empty_subst then
-	  update_subst sub_alias (map_mbid farg_id mp None)
+	  update_subst sub_alias (map_mbid farg_id mp (Some resolve))
 	else
-	  let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+	  let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
 	  let sub_alias' =  update_subst sub_alias sub1' in
-	    join sub1' sub_alias'
+		     join sub1' sub_alias'
       in
-      let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
-      let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
-	(match mbids with
-	   | mbid::mbids ->
-               let resolve =
-		 Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
-		 (* application outside the kernel, only for substitutive
-                    objects (that are all non-logical objects) *)
-		((join 
-		    (join subst sub3)
-		       (map_mbid mbid mp (Some resolve)))
-		       , mbids, msid, objs)
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments")
+      let sub3 = join sub3 (update_subst sub_alias 
+			      (map_mbid farg_id mp (Some resolve))) in
+	(* application outside the kernel, only for substitutive
+           objects (that are all non-logical objects) *)
+	((join 
+	    (join subst sub3)
+	    (map_mbid mbid mp (Some resolve)))
+	   , mbids, msid, objs)
   | MSEapply (_,mexpr) ->
       Modops.error_application_to_not_path mexpr
   | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty
@@ -1061,12 +1064,9 @@ let rec update_include (sub,mbids,msid,objs) =
     | (id,obj)::tail ->
 	if object_tag obj = "INCLUDE" then
 	  let ((me,is_mod),substobjs,substituted) = out_include obj in
-	    if not (is_mod) then
-	      let substobjs' = update_include substobjs in
-                (id, in_include ((me,true),substobjs',substituted))::
-		  (replace_include tail)
-	    else
-		  (id,obj)::(replace_include tail)
+	  let substobjs' = update_include substobjs in
+            (id, in_include ((me,true),substobjs',substituted))::
+	      (replace_include tail)
 	else
 	  (id,obj)::(replace_include tail)
   in
@@ -1142,7 +1142,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
       | _ ->
 	  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
 	  let (sub,mbids,msid,objs) = substobjs in
-	  let sub' = subst_key (map_msid msid mp) sub in
+	  let sub' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in
 	  let substobjs = (join sub sub',mbids,msid,objs) in
 	  let substituted = subst_substobjs dir mp substobjs in
 	    ignore (add_leaf
diff --git a/library/impargs.ml b/library/impargs.ml
index 2b2c607c..14f88728 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: impargs.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Util
 open Names
@@ -26,8 +26,7 @@ open Termops
 (*s Flags governing the computation of implicit arguments *)
 
 type implicits_flags = {
-  main : bool;
-  manual : bool;                     (* automatic or manual only *)
+  auto : bool;                     (* automatic or manual only *)
   strict : bool;                   (* true = strict *)
   strongly_strict : bool;            (* true = strongly strict *)
   reversible_pattern : bool;
@@ -38,8 +37,7 @@ type implicits_flags = {
 (* les implicites sont stricts par défaut en v8 *)
 
 let implicit_args = ref { 
-  main = false;
-  manual = false;
+  auto = false;
   strict = true;
   strongly_strict = false;
   reversible_pattern = false;
@@ -48,11 +46,7 @@ let implicit_args = ref {
 }
 
 let make_implicit_args flag =
-  implicit_args := { !implicit_args with main = flag }
-
-let make_manual_implicit_args flag =
-  implicit_args := { !implicit_args with main = if flag then true else !implicit_args.main;
-    manual = flag }
+  implicit_args := { !implicit_args with auto = flag }
 
 let make_strict_implicit_args flag =
   implicit_args := { !implicit_args with strict = flag }
@@ -69,9 +63,7 @@ let make_contextual_implicit_args flag =
 let make_maximal_implicit_args flag =
   implicit_args := { !implicit_args with maximal = flag }
 
-let is_implicit_args () = !implicit_args.main
-let is_manual_implicit_args () = !implicit_args.manual
-let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ())
+let is_implicit_args () = !implicit_args.auto
 let is_strict_implicit_args () = !implicit_args.strict
 let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
 let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -316,10 +308,10 @@ let const v _ = v
 let compute_implicits_auto env f manual t =
   match manual with
   | [] -> 
-      let l = compute_implicits_flags env f false t in
-	if f.manual then List.map (const None) l
-	else prepare_implicits f l
-  | _ -> compute_manual_implicits env f t (not f.manual) manual
+      if not f.auto then []
+      else let l = compute_implicits_flags env f false t in
+	     prepare_implicits f l
+  | _ -> compute_manual_implicits env f t f.auto manual
 	
 let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
 
@@ -523,7 +515,7 @@ let rebuild_implicits (req,l) =
       | ImplManual m -> 
 	  let oldimpls = snd (List.hd l) in
 	  let auto = 
-	    if flags.main then
+	    if flags.auto then
 	      let newimpls = compute_global_implicits flags [] ref in
 		merge_impls oldimpls newimpls
 	    else oldimpls
@@ -549,32 +541,30 @@ let declare_implicits_gen req flags ref =
   add_anonymous_leaf (inImplicits (req,[ref,imps]))
 
 let declare_implicits local ref =
-  let flags = { !implicit_args with main = true } in
+  let flags = { !implicit_args with auto = true } in
   let req = 
     if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
-  declare_implicits_gen req flags ref
-
+    declare_implicits_gen req flags ref
+      
 let declare_var_implicits id =
-  if !implicit_args.main then
-    declare_implicits_gen ImplLocal !implicit_args (VarRef id)
+  let flags = !implicit_args in
+    declare_implicits_gen ImplLocal flags (VarRef id)
 
 let declare_constant_implicits con =
-  if !implicit_args.main then
-    let flags = !implicit_args in
+  let flags = !implicit_args in
     declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
 
 let declare_mib_implicits kn =
-  if !implicit_args.main then
-    let flags = !implicit_args in
-    let imps = array_map_to_list
-      (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
-      (compute_mib_implicits flags [] kn) in
+  let flags = !implicit_args in
+  let imps = array_map_to_list
+    (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
+    (compute_mib_implicits flags [] kn) in
     add_anonymous_leaf
       (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
-
+      
 (* Declare manual implicits *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool) 
-
+  
 let compute_implicits_with_manual env typ enriching l = 
   compute_manual_implicits env !implicit_args typ enriching l
 
@@ -582,7 +572,7 @@ let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
   let t = Global.type_of_global ref in
-  let enriching = Option.default (is_auto_implicit_args ()) enriching in
+  let enriching = Option.default flags.auto enriching in
   let l' = compute_manual_implicits env flags t enriching l in
   let req =
     if local or isVarRef ref then ImplLocal
diff --git a/library/impargs.mli b/library/impargs.mli
index a363effa..c1f119e6 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: impargs.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: impargs.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -20,7 +20,6 @@ open Nametab
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
-val make_manual_implicit_args : bool -> unit
 val make_strict_implicit_args : bool -> unit
 val make_strongly_strict_implicit_args : bool -> unit
 val make_reversible_pattern_implicit_args : bool -> unit
@@ -28,7 +27,6 @@ val make_contextual_implicit_args : bool -> unit
 val make_maximal_implicit_args : bool -> unit
 
 val is_implicit_args : unit -> bool
-val is_manual_implicit_args : unit -> bool
 val is_strict_implicit_args : unit -> bool
 val is_strongly_strict_implicit_args : unit -> bool
 val is_reversible_pattern_implicit_args : unit -> bool
diff --git a/library/lib.ml b/library/lib.ml
index 88bcd0b8..4a124cec 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -452,7 +452,7 @@ type variable_context = variable_info list
 type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
@@ -460,13 +460,19 @@ let add_section () =
 let add_section_variable id impl keep =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
+    | (vars,repl,abs)::sl ->
+	sectab := ((id,impl,keep)::vars,repl,abs)::sl
 
-let rec extract_hyps = function
-  | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
-  | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
-  | (id::idl,hyps) -> extract_hyps (idl,hyps)
-  | [], _ -> []
+let extract_hyps (secs,ohyps) =
+  let rec aux = function
+    | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
+    | ((id,impl,Some (ty,keep))::idl,hyps) -> 
+	if List.exists (fun (id,_,_) -> List.mem id keep) ohyps then
+	  (id,impl,None,ty) :: aux (idl,hyps)
+	else aux (idl,hyps)
+    | (id::idl,hyps) -> aux (idl,hyps)
+    | [], _ -> []
+  in aux (secs,ohyps)
 
 let instance_from_variable_context sign =
   let rec inst_rec = function
diff --git a/library/lib.mli b/library/lib.mli
index 23af7c17..dacfed59 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lib.mli 11671 2008-12-12 12:43:03Z herbelin $ i*)
+(*i $Id: lib.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 
 (*s This module provides a general mechanism to keep a trace of all operations
@@ -182,7 +182,9 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont
 val section_instance : Libnames.global_reference -> Names.identifier array
 val is_in_section : Libnames.global_reference -> bool
 
-val add_section_variable : Names.identifier -> binding_kind -> Term.types option -> unit
+val add_section_variable : Names.identifier -> binding_kind -> 
+  (Term.types * Names.identifier list) option -> unit
+
 val add_section_constant : Names.constant -> Sign.named_context -> unit
 val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
 val replacement_context : unit ->
diff --git a/library/states.ml b/library/states.ml
index 7f7fef47..c81f9614 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 11313 2008-08-07 11:15:03Z barras $ *)
+(* $Id: states.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
 
 open System
 
@@ -35,3 +35,10 @@ let with_heavy_rollback f x =
     f x
   with reraise ->
     (unfreeze st; raise reraise)
+
+let with_state_protection f x =
+  let st = freeze () in
+  try 
+    let a = f x in unfreeze st; a
+  with reraise ->
+    (unfreeze st; raise reraise)
diff --git a/library/states.mli b/library/states.mli
index eff046ef..210e06b2 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: states.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: states.mli 12080 2009-04-11 16:56:20Z herbelin $ i*)
 
 (*s States of the system. In that module, we provide functions to get
   and set the state of the whole system. Internally, it is done by
@@ -26,4 +26,9 @@ val unfreeze : state -> unit
 
 val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
 
+(*s [with_state_protection f x] applies [f] to [x] and restores the
+  state of the whole system as it was before the evaluation of f *)
+
+val with_state_protection : ('a -> 'b) -> 'a -> 'b
+
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7bebf6db..ad093507 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_tactic.ml4 11741 2009-01-03 14:34:39Z herbelin $ *)
+(* $Id: g_tactic.ml4 12009 2009-03-23 22:55:37Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -72,15 +72,16 @@ let test_lpar_id_colon =
 let check_for_coloneq =
   Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
-      let rec skip_to_rpar n =
+      let rec skip_to_rpar p n =
 	match list_last (Stream.npeek n strm) with
-        | ("",")") -> n+1
+        | ("","(") -> skip_to_rpar (p+1) (n+1)
+        | ("",")") -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1)
 	| ("",".") -> raise Stream.Failure
-	| _ -> skip_to_rpar (n+1) in
+	| _ -> skip_to_rpar p (n+1) in
       let rec skip_names n =
 	match list_last (Stream.npeek n strm) with
         | ("IDENT",_) | ("","_") -> skip_names (n+1)
-	| ("",":") -> skip_to_rpar (n+1) (* skip a constr *)
+	| ("",":") -> skip_to_rpar 0 (n+1) (* skip a constr *)
 	| _ -> raise Stream.Failure in
       let rec skip_binders n =
 	match list_last (Stream.npeek n strm) with
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f960492e..b2d67e1c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_vernac.ml4 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 
 open Pp
@@ -447,10 +447,13 @@ GEXTEND Gram
 	  CWith_Module (fqid,qid)
       ] ]
   ;
-  module_type:
+  module_type_atom:
     [ [ qid = qualid -> CMTEident qid
-(* ... *)
-      | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) 
+      | mty = module_type_atom; me = module_expr_atom -> CMTEapply (mty,me) 
+      ] ]
+  ;
+  module_type:
+    [ [ mty = module_type_atom -> mty
       | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl)
       ] ]
   ;
@@ -700,7 +703,8 @@ GEXTEND Gram
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
       | IDENT "Implicit"; qid = global -> PrintImplicit qid
       | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
-      | IDENT "Assumptions"; qid = global -> PrintAssumptions qid ] ]
+      | IDENT "Assumptions"; qid = global -> PrintAssumptions (false, qid)
+      | IDENT "Opaque"; IDENT "Dependencies"; qid = global -> PrintAssumptions (true, qid) ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d0a9c3d8..d2d81cd1 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
 
-(*i $Id: pcoq.ml4 11784 2009-01-14 11:36:32Z herbelin $ i*)
+(*i $Id: pcoq.ml4 12055 2009-04-07 18:19:05Z herbelin $ i*)
 
 open Pp
 open Util
@@ -735,7 +735,10 @@ let is_binder_level from e =
 
 let rec symbol_of_production assoc from forpat typ =
   if is_binder_level from typ then
-    Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200")
+    if forpat then
+      Gramext.Snterml (Gram.Entry.obj Constr.pattern,"200")
+    else
+      Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200")
   else if is_self from typ then
     Gramext.Sself
   else
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 78c63ca2..5f4ea5a6 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)  
+(* $Id: ppvernac.ml 12187 2009-06-13 19:36:59Z msozeau $ *)  
 
 open Pp
 open Names
@@ -897,7 +897,8 @@ let rec pr_vernac = function
 	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
 (* spiwack: command printing all the axioms and section variables used in a 
          term *)
-	| PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
+	| PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
+	    ++spc()++pr_reference qid
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc -> 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 5543a31c..1e50bc51 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
  * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
  *)
 
-(* $Id: prettyp.ml 11622 2008-11-23 08:45:56Z herbelin $ *)
+(* $Id: prettyp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -107,8 +107,9 @@ let need_expansion impl ref =
   let typ = Global.type_of_global ref in
   let ctx = fst (decompose_prod_assum typ) in
   let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
-  impl <> [] & let _,lastimpl = list_chop nprods impl in
-  List.filter is_status_implicit lastimpl <> []
+  impl <> [] & List.length impl >= nprods &
+    let _,lastimpl = list_chop nprods impl in
+      List.filter is_status_implicit lastimpl <> []
 
 type opacity =
   | FullyOpaque
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 10034dd9..0c673fbd 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: printer.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: printer.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -431,10 +431,11 @@ let pr_prim_rule = function
        (str"cut " ++ pr_constr t ++ 
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 	
-  | FixRule (f,n,[]) ->
+  | FixRule (f,n,[],_) ->
       (str"fix " ++ pr_id f ++ str"/" ++ int n)
       
-  | FixRule (f,n,others) -> 
+  | FixRule (f,n,others,j) -> 
+      if j<>0 then warning "Unsupported printing of \"fix\"";
       let rec print_mut = function
 	| (f,n,ar)::oth -> 
            pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
@@ -442,10 +443,11 @@ let pr_prim_rule = function
       (str"fix " ++ pr_id f ++ str"/" ++ int n ++
          str" with " ++ print_mut others)
 
-  | Cofix (f,[]) ->
+  | Cofix (f,[],_) ->
       (str"cofix " ++ pr_id f)
 
-  | Cofix (f,others) ->
+  | Cofix (f,others,j) ->
+      if j<>0 then warning "Unsupported printing of \"fix\"";
       let rec print_mut = function
 	| (f,ar)::oth ->
 	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
@@ -499,10 +501,10 @@ let pr_assumptionset env s =
   if (Environ.ContextObjectMap.is_empty s) then
     str "Closed under the global context"
   else
-    let (vars,axioms) =
-      Environ.ContextObjectMap.fold (fun o typ r ->
-	let (v,a) = r in
-	match o with
+    let (vars,axioms,opaque) =
+      Environ.ContextObjectMap.fold (fun t typ r ->
+	let (v,a,o) = r in
+	match t with
 	| Variable id -> (  Some (
 	                      Option.default (fnl ()) v 
 			   ++ str (string_of_id id)
@@ -511,7 +513,7 @@ let pr_assumptionset env s =
 	                   ++ fnl ()
 			    )
 	                 ,
-	                   a )
+	                   a, o)
 	| Axiom kn    -> ( v ,
 			     Some (
 			      Option.default (fnl ()) a
@@ -520,16 +522,28 @@ let pr_assumptionset env s =
 	                   ++ pr_ltype typ
 	                   ++ fnl ()
 			     )
+			 , o
 			 )
-	)
-	s (None,None)
+	| Opaque kn    -> ( v , a ,
+			     Some (
+			      Option.default (fnl ()) o
+			   ++ (pr_constant env kn)
+	                   ++ str " : "
+	                   ++ pr_ltype typ
+	                   ++ fnl ()
+			     )
+			 )
+      )
+	s (None,None,None)
     in
-    let (vars,axioms) = 
+    let (vars,axioms,opaque) = 
       ( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
-	Option.map (fun p -> str "Axioms:" ++ p) axioms 
+	Option.map (fun p -> str "Axioms:" ++ p) axioms ,
+	Option.map (fun p -> str "Opaque constants:" ++ p) opaque
       )
     in
     (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
+      ++ (Option.default (mt ()) opaque)
 
 let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a4880f5e..c2d8921e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *)
 
 open Util
 open Names
@@ -130,7 +130,7 @@ let push_rel_defs =
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
 
-let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
+let regeneralize_rel i k j = if j = i+k then k+1 else j
 
 let rec regeneralize_index i k t = match kind_of_term t with
   | Rel j when j = i+k -> mkRel (k+1)
@@ -605,19 +605,13 @@ let find_dependencies_signature deps_in_rhs typs =
   let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
   List.map (fun (_,deps,_) -> deps) l
 
-(******)
+(* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
+   and xn:Tn has just been regeneralized into x:Tn so that the terms
+   to match are now to be considered in the context xp:Tp,...,x1:T1,x:Tn |-.
 
-(* A Pushed term to match has just been substituted by some
-   constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
-   match 
-
-   - all terms to match and to push (dependent on t by definition)
-     must have (Rel depth) substituted by t and Rel's>depth lifted by n
-   - all pushed terms to match (non dependent on t by definition) must
-     be lifted by n
-
-  We start with depth=1
-*)
+   [regeneralize_index_tomatch n tomatch] updates t1..tq so that
+   former references to xn are now references to x. Note that t1..tq
+   are already adjusted to the context xp:Tp,...,x1:T1,x:Tn |-. *)
 
 let regeneralize_index_tomatch n =
   let rec genrec depth = function
@@ -661,6 +655,13 @@ let replace_tomatch n c =
 let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
 let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
 
+(* [liftn_tomatch_stack]: a term to match has just been substituted by
+   some constructor t = (ci x1...xn) and the terms x1 ... xn have been
+   added to match; all pushed terms to match must be lifted by n
+   (knowing that [Abstract] introduces a binder in the list of pushed
+   terms to match).
+*)
+
 let rec liftn_tomatch_stack n depth = function
   | [] -> []
   | Pushed ((c,tm),l,dep)::rest ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4c5ebe3e..043a326d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *)
 
 open Pp
 open Util
@@ -474,11 +474,11 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   let (evd',ks,_) =
     List.fold_left
       (fun (i,ks,m) b ->
-	 if m=0 then (i,t2::ks, n-1) else
+	 if m=n then (i,t2::ks, m-1) else
 	 let dloc = (dummy_loc,InternalHole) in
          let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
-	 (i', ev :: ks, n - 1))
-      (evd,[],n) bs
+	 (i', ev :: ks, m - 1))
+      (evd,[],List.length bs - 1) bs
   in
   ise_and evd'
     [(fun i ->
@@ -505,7 +505,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
       if is_defined_evar i ev1 then
 	evar_conv_x env i CONV t2 (mkEvar ev1)
       else
-	solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
+	solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find (evars_of evd) evk in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c0c0b941..994da427 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *)
 
 open Util
 open Pp
@@ -673,7 +673,11 @@ let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_bind
 
 let invert_arg env k sigma (evk,args_in_env) c_in_env_extended_with_k_binders =
   let subst_in_env = make_projectable_subst sigma (Evd.find sigma evk) args_in_env in
-  invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders
+  let res = invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders in
+  match res with
+  | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
+  | _ -> res
+
 
 let effective_projections =
   map_succeed (function Invertible c -> c | _ -> failwith"")
@@ -836,7 +840,7 @@ let expand_rhs env sigma subst rhs =
 exception NotInvertibleUsingOurAlgorithm of constr
 exception NotEnoughInformationToProgress
 
-let rec invert_definition env evd (evk,argsv as ev) rhs =
+let rec invert_definition choose env evd (evk,argsv as ev) rhs =
   let evdref = ref evd in
   let progress = ref false in
   let evi = Evd.find (evars_of evd) evk in
@@ -847,7 +851,11 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
     (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
     try 
       let sols = find_projectable_vars true env (evars_of !evdref) t subst in
-      let c, p = filter_solution sols in
+      let c, p = match sols with
+	| [] -> raise Not_found
+	| [id,p] -> (mkVar id, p)
+	| (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
+      in
       let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in
       let evd = do_projection_effects evar_define env ty !evdref p in
       evdref := evd;
@@ -923,9 +931,9 @@ and occur_existential evm c =
     | _ -> iter_constr occrec c
   in try occrec c; false with Occur -> true
 
-and evar_define env (evk,_ as ev) rhs evd =
+and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
   try
-    let (evd',body) = invert_definition env evd ev rhs in
+    let (evd',body) = invert_definition choose env evd ev rhs in
     if occur_meta body then error "Meta cannot occur in evar body.";
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
@@ -1120,7 +1128,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
  * if the problem couldn't be solved. *)
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
+let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
     let t2 = whd_evar (evars_of evd) t2 in
     let evd = match kind_of_term t2 with
@@ -1132,15 +1140,18 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
 	    then solve_evar_evar evar_define env evd ev1 ev2
 	    else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
       | _ ->
-	  let evd = evar_define env ev1 t2 evd in
+	  let evd = evar_define ~choose env ev1 t2 evd in
 	  let evm = evars_of evd in
 	  let evi = Evd.find evm evk1 in
 	    if occur_existential evm evi.evar_concl then
 	      let evenv = evar_env evi in
 	      let evc = nf_isevar evd evi.evar_concl in
-	      let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in
-	      let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
-		add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+		match evi.evar_body with 
+		| Evar_defined body -> 
+		    let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
+		      add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+		| Evar_empty -> (* Resulted in a constraint *) 
+		    evd
 	    else evd
     in
     let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
@@ -1251,8 +1262,8 @@ let define_evar_as_abstraction abs evd (ev,args) =
   let evrng =
     fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
   let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
-  (evd3,prod')
-
+    (evd3,prod')
+      
 let define_evar_as_product evd (ev,args) =
   define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
 
@@ -1263,7 +1274,6 @@ let define_evar_as_sort evd (ev,args) =
   let s = new_Type () in
   Evd.evar_define ev s evd, destSort s
 
-
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
 
@@ -1275,27 +1285,26 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
    an evar instantiate it with the product of 2 new evars. *)
 
 let split_tycon loc env evd tycon = 
-  let rec real_split c = 
-    let sigma = evars_of evd in
-    let t = whd_betadeltaiota env sigma c in
+  let rec real_split evd c = 
+    let t = whd_betadeltaiota env (Evd.evars_of evd) c in
       match kind_of_term t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
 	| Evar ev when not (Evd.is_defined_evar evd ev) ->
 	    let (evd',prod) = define_evar_as_product evd ev in
 	    let (_,dom,rng) = destProd prod in
 	      evd',(Anonymous, dom, rng)
-	| _ -> error_not_product_loc loc env sigma c
+	| _ -> error_not_product_loc loc env (Evd.evars_of evd) c
   in
     match tycon with
       | None -> evd,(Anonymous,None,None)
       | Some (abs, c) ->
 	  (match abs with
 	       None -> 
-		 let evd', (n, dom, rng) = real_split c in
+		 let evd', (n, dom, rng) = real_split evd c in
 		   evd', (n, mk_tycon dom, mk_tycon rng)
 	     | Some (init, cur) ->
 		 if cur = 0 then 
-		   let evd', (x, dom, rng) = real_split c in
+		   let evd', (x, dom, rng) = real_split evd c in
 		     evd, (Anonymous, 
 			  Some (None, dom), 
 			  Some (None, rng))
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a687fdf0..cb54f400 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evarutil.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
+(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -53,11 +53,11 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 (***********************************************************)
 (* Instantiate evars *)
 
-(* [evar_define env ev c] try to instantiate [ev] with [c] (typed in [env]),
+(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
    possibly solving related unification problems, possibly leaving open
-   some problems that cannot be solved in a unique way;
-   failed if the instance is not valid for the given [ev] *)
-val evar_define : env -> existential -> constr -> evar_defs -> evar_defs
+   some problems that cannot be solved in a unique way (except if choose is
+   true); fails if the instance is not valid for the given [ev] *)
+val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs
 
 (***********************************************************)
 (* Evars/Metas switching... *)
@@ -80,7 +80,7 @@ val solve_refl :
     evar_defs
 val solve_simple_eqn :
   (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-  -> env ->  evar_defs -> conv_pb * existential * constr ->
+  -> ?choose:bool -> env ->  evar_defs -> conv_pb * existential * constr ->
     evar_defs * bool
 
 (* [check_evars env initial_sigma extended_sigma c] fails if some
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1cac9011..c0f820a2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: pretyping.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
 
 open Pp
 open Util
@@ -443,7 +443,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 	    
     | RLetIn(loc,name,c1,c2)      ->
-	let j = pretype empty_tycon env evdref lvar c1 in
+	let j = 
+	  match c1 with
+	  | RCast (loc, c, CastConv (DEFAULTcast, t)) ->
+	      let tj = pretype_type empty_valcon env evdref lvar t in		
+		pretype (mk_tycon tj.utj_val) env evdref lvar c
+	  | _ -> pretype empty_tycon env evdref lvar c1
+	in
 	let t = refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
         let tycon = lift_tycon 1 tycon in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7c4023b9..711f332e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: recordops.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: recordops.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Util
 open Pp
@@ -65,8 +65,11 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
     if projs' == projs && kn' == kn && id' == id then obj else
       ((kn',i),id',kl,projs')
 
+let discharge_constructor (ind, n) = 
+  (Lib.discharge_inductive ind, n)
+
 let discharge_structure (_,(ind,id,kl,projs)) =
-  Some (Lib.discharge_inductive ind, id, kl,
+  Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
         List.map (Option.map Lib.discharge_con) projs)
 
 let (inStruc,outStruc) =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f93212f8..4f38fbb3 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termops.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(* $Id: termops.ml 12058 2009-04-08 10:54:59Z herbelin $ *)
 
 open Pp
 open Util
@@ -1017,6 +1017,15 @@ let assums_of_rel_context sign =
         | None -> (na, t)::l)
     sign ~init:[]
 
+let fold_map_rel_context f env sign =
+  let rec aux env acc = function
+    | d::sign ->
+	aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
+    | [] ->
+	acc
+  in
+  aux env [] (List.rev sign)
+
 let map_rel_context_with_binders f sign =
   let rec aux k = function
     | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index d44c762e..e0bbe7b5 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: termops.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: termops.mli 12058 2009-04-08 10:54:59Z herbelin $ i*)
 
 open Util
 open Pp
@@ -241,6 +241,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val substl_rel_context : constr list -> rel_context -> rel_context
+val fold_map_rel_context :
+  (env -> constr -> constr) -> env -> rel_context -> rel_context
 val map_rel_context_with_binders : 
   (int -> constr -> constr) -> rel_context -> rel_context
 val fold_named_context_both_sides :
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8680e578..216a0611 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: typeclasses.ml 12189 2009-06-15 05:08:44Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -381,7 +381,7 @@ let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses (Evd.evars_of evd)) then evd
   else
-    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
+    !solve_instanciations_problem env evd onlyargs split fail
 
 let resolve_one_typeclass env evm t =
   !solve_instanciation_problem env evm t
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fb29196c..bfd601e2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *)
 
 open Pp
 open Util
@@ -492,7 +492,7 @@ let w_coerce env evd mv c =
 let unify_to_type env evd flags c u =
   let sigma = evars_of evd in
   let c = refresh_universes c in
-  let t = get_type_of_with_meta env sigma (metas_of evd) c in
+  let t = get_type_of_with_meta env sigma (List.map (on_snd (nf_meta evd)) (metas_of evd)) (nf_meta evd c) in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
   let u = Tacred.hnf_constr env sigma u in
   try unify_0 env sigma Cumul flags t u
@@ -500,7 +500,7 @@ let unify_to_type env evd flags c u =
 
 let unify_type env evd flags mv c =
   let mvty = Typing.meta_type evd mv in
-  if occur_meta_or_existential mvty then
+  if occur_meta_or_existential mvty or is_arity env (evars_of evd) mvty then
     unify_to_type env evd flags c mvty
   else ([],[])
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index f5204be5..769a9572 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenvtac.ml 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: clenvtac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Pp
 open Util
@@ -25,7 +25,6 @@ open Logic
 open Reduction
 open Reductionops
 open Tacmach
-open Evar_refiner
 open Rawterm
 open Pattern
 open Tacexpr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d19d81e0..f4613f8d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: evar_refiner.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Util
 open Names
@@ -15,6 +15,7 @@ open Evd
 open Sign
 open Proof_trees
 open Refiner
+open Pretyping
 
 (******************************************)
 (* Instantiation of existential variables *)
@@ -22,21 +23,21 @@ open Refiner
 
 (* w_tactic pour instantiate *) 
 
-let w_refine evk rawc evd =
+let w_refine evk (ltac_vars,rawc) evd =
   if Evd.is_defined (evars_of evd) evk then 
     error "Instantiate called on already-defined evar";
   let e_info = Evd.find (evars_of evd) evk in
   let env = Evd.evar_env e_info in
-  let sigma,typed_c =
-    try Pretyping.Default.understand_tcc ~resolve_classes:false
-      (evars_of evd) env ~expected_type:e_info.evar_concl rawc
+  let evd',typed_c =
+    try Pretyping.Default.understand_ltac 
+      (evars_of evd) env ltac_vars (OfType (Some e_info.evar_concl)) rawc
     with _ ->
       let loc = Rawterm.loc_of_rawconstr rawc in
       user_err_loc 
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
   in
-    evar_define evk typed_c (evars_reset_evd sigma evd)
+    evar_define evk typed_c (evars_reset_evd (evars_of evd') evd)
 
 (* vernac command Existential *)
 
@@ -55,5 +56,5 @@ let instantiate_pf_com n com pfts =
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in 
   let evd = create_goal_evar_defs sigma in
-  let evd' = w_refine evk rawc evd in
+  let evd' = w_refine evk (([],[]),rawc) evd in
     change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index baa6b19a..a42b11a4 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evar_refiner.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id: evar_refiner.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -14,11 +14,14 @@ open Term
 open Environ
 open Evd
 open Refiner
+open Pretyping
+open Rawterm
 (*i*)
 
 (* Refinement of existential variables. *)
 
-val w_refine : evar -> Rawterm.rawconstr  -> evar_defs -> evar_defs
+val w_refine : evar -> (var_map * unbound_ltac_var_map) * rawconstr -> 
+  evar_defs -> evar_defs
 
 val instantiate_pf_com :
   int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3e758eb6..caf6f56b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -517,7 +517,7 @@ let prim_refiner r sigma goal =
         let sg2 = mk_goal sign cl in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
-    | FixRule (f,n,rest) ->
+    | FixRule (f,n,rest,j) ->
      	let rec check_ind env k cl = 
           match kind_of_term (strip_outer_cast cl) with 
             | Prod (na,c1,b) -> 
@@ -531,7 +531,8 @@ let prim_refiner r sigma goal =
             | _ -> error "Not enough products."
 	in
 	let (sp,_) = check_ind env n cl in
-	let all = (f,n,cl)::rest in
+	let firsts,lasts = list_chop j rest in
+	let all = firsts@(f,n,cl)::lasts in
      	let rec mk_sign sign = function 
 	  | (f,n,ar)::oth ->
 	      let (sp',_)  = check_ind env n ar in 
@@ -539,14 +540,15 @@ let prim_refiner r sigma goal =
 		error ("Fixpoints should be on the same " ^ 
 		       "mutual inductive declaration.");
 	      if !check && mem_named_context f (named_context_of_val sign) then
-		error "Name already used in the environment";
+		error
+		  ("Name "^string_of_id f^" already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] -> 
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
 	in 
 	  (mk_sign sign all, sigma)
 	
-    | Cofix (f,others) ->
+    | Cofix (f,others,j) ->
      	let rec check_is_coind env cl = 
 	  let b = whd_betadeltaiota env sigma cl in
           match kind_of_term b with
@@ -558,7 +560,8 @@ let prim_refiner r sigma goal =
 		  error ("All methods must construct elements " ^
 			  "in coinductive types.")
 	in
-	let all = (f,cl)::others in
+	let firsts,lasts = list_chop j others in
+	let all = firsts@(f,cl)::lasts in
      	List.iter (fun (_,c) -> check_is_coind env c) all;
         let rec mk_sign sign = function 
           | (f,ar)::oth ->
@@ -687,24 +690,26 @@ let prim_extractor subfun vl pft =
 	    mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
                     subfun (add_proof_var id vl) spf2)
 
-      | Some (Prim (FixRule (f,n,others)),spfl) ->
-	  let all = Array.of_list ((f,n,cl)::others) in
+      | Some (Prim (FixRule (f,n,others,j)),spfl) ->
+	  let firsts,lasts = list_chop j others in
+	  let all = Array.of_list (firsts@(f,n,cl)::lasts) in
 	  let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
 	  let names = Array.map (fun (f,_,_) -> Name f) all in
 	  let vn = Array.map (fun (_,n,_) -> n-1) all in
 	  let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
             (add_proof_var f vl) others in
 	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkFix ((vn,0),(names,lcty,lfix))	
+	    mkFix ((vn,j),(names,lcty,lfix))	
 
-      | Some (Prim (Cofix (f,others)),spfl) ->
-	  let all = Array.of_list ((f,cl)::others) in
+      | Some (Prim (Cofix (f,others,j)),spfl) ->
+	  let firsts,lasts = list_chop j others in
+	  let all = Array.of_list (firsts@(f,cl)::lasts) in
 	  let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
 	  let names  = Array.map (fun (f,_) -> Name f) all in
 	  let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
             (add_proof_var f vl) others in 
 	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkCoFix (0,(names,lcty,lfix))
+	    mkCoFix (j,(names,lcty,lfix))
 	      
       | Some (Prim (Refine c),spfl) ->
 	  let mvl = collect_meta_variables c in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 1e673853..150fb89f 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(*i $Id: proof_type.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
 
 (*i*)
 open Environ
@@ -29,8 +29,8 @@ open Pattern
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
-  | FixRule of identifier * int * (identifier * int * constr) list
-  | Cofix of identifier * (identifier * constr) list
+  | FixRule of identifier * int * (identifier * int * constr) list * int
+  | Cofix of identifier * (identifier * constr) list * int
   | Refine of constr
   | Convert_concl of types * cast_kind
   | Convert_hyp of named_declaration
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 21cd8b28..c80e126f 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: proof_type.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
 
 (*i*)
 open Environ
@@ -29,8 +29,8 @@ open Pattern
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
-  | FixRule of identifier * int * (identifier * int * constr) list
-  | Cofix of identifier * (identifier * constr) list
+  | FixRule of identifier * int * (identifier * int * constr) list * int
+  | Cofix of identifier * (identifier * constr) list * int
   | Refine of constr
   | Convert_concl of types * cast_kind 
   | Convert_hyp of named_declaration
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6c4f7b5e..b740baa8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tacmach.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -211,11 +211,15 @@ let rec rename_hyp_no_check l gl = match l with
       tclTHEN (refiner (Prim (Rename (id1,id2)))) 
 	(rename_hyp_no_check l) gl
 
-let mutual_fix f n others gl = 
-  with_check (refiner (Prim (FixRule (f,n,others)))) gl
+let mutual_fix_with_index f n others j gl =
+  with_check (refiner (Prim (FixRule (f,n,others,j)))) gl
 
-let mutual_cofix f others gl = 
-  with_check (refiner (Prim (Cofix (f,others)))) gl
+let mutual_fix f n others = mutual_fix_with_index f n others 0
+
+let mutual_cofix_with_index f others j gl =
+  with_check (refiner (Prim (Cofix (f,others,j)))) gl
+
+let mutual_cofix f others = mutual_cofix_with_index f others 0
     
 (* Versions with consistency checks *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cdcb8bfd..37acf850 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacmach.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: tacmach.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -137,6 +137,10 @@ val order_hyps : identifier list -> tactic
 val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+val mutual_fix_with_index :
+  identifier -> int -> (identifier * int * constr) list -> int -> tactic
+val mutual_cofix_with_index : 
+  identifier -> (identifier * constr) list -> int -> tactic
 
 (*s The most primitive tactics with consistency and type checking *)
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1212656b..36136a6c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: auto.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: auto.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -150,10 +150,13 @@ module Hint_db = struct
     try Constr_map.find key db.hintdb_map
     with Not_found -> empty_se
       
+  let map_none db = 
+    Sort.merge pri_order db.hintdb_nopat []
+      
   let map_all k db =
     let (l,l',_) = find k db in
       Sort.merge pri_order (db.hintdb_nopat @ l) l'
-   
+
   let map_auto (k,c) db =
     let st = if db.use_dn then Some db.hintdb_state else None in
     let l' = lookup_tacs (k,c) st (find k db) in
@@ -637,26 +640,24 @@ let print_hint_ref ref =  ppnl(pr_hint_ref ref)
 
 let pr_hint_term cl = 
   try 
-    let (hdc,args) = head_constr_bound cl in
-    let hd = head_of_constr_reference hdc in
     let dbs = Hintdbmap.to_list !searchtable in
     let valid_dbs = 
-      if occur_existential cl then 
-	map_succeed 
-	  (fun (name, db) -> (name, db, Hint_db.map_all hd db)) 
-	  dbs
-      else 
-	map_succeed 
-	  (fun (name, db) -> 
-	     (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) 
-	  dbs
-    in 
-    if valid_dbs = [] then 
-      (str "No hint applicable for current goal")
-    else
-      (str "Applicable Hints :" ++ fnl () ++
-	 hov 0 (prlist pr_hints_db valid_dbs))
-  with Bound | Match_failure _ | Failure _ -> 
+      let fn = try 
+	  let (hdc,args) = head_constr_bound cl in
+	  let hd = head_of_constr_reference hdc in
+	    if occur_existential cl then
+	      Hint_db.map_all hd
+	    else Hint_db.map_auto (hd, applist (hdc,args))
+	with Bound -> Hint_db.map_none
+      in
+	map_succeed (fun (name, db) -> (name, db, fn db)) dbs
+    in
+      if valid_dbs = [] then 
+	(str "No hint applicable for current goal")
+      else
+	(str "Applicable Hints :" ++ fnl () ++
+	    hov 0 (prlist pr_hints_db valid_dbs))
+  with Match_failure _ | Failure _ -> 
     (str "No hint applicable for current goal")
 
 let error_no_such_hint_database x =
@@ -795,6 +796,13 @@ let flags_of_state st =
   {auto_unif_flags with 
     modulo_conv_on_closed_terms = Some st; modulo_delta = st}
 
+let hintmap_of hdc concl =
+  match hdc with
+  | None -> Hint_db.map_none
+  | Some hdc ->
+      if occur_existential concl then Hint_db.map_all hdc
+      else Hint_db.map_auto (hdc,concl)
+	
 let rec trivial_fail_db mod_delta db_list local_db gl =
   let intro_tac = 
     tclTHEN intro 
@@ -808,12 +816,8 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
        (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
 
 and my_find_search_nodelta db_list local_db hdc concl =
-  if occur_existential concl then
-    List.map (fun hint -> (None,hint))
-      (list_map_append (Hint_db.map_all hdc) (local_db::db_list))
-  else
-    List.map (fun hint -> (None,hint))
-      (list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list))
+  List.map (fun hint -> (None,hint)) 
+    (list_map_append (hintmap_of hdc concl) (local_db::db_list))
 
 and my_find_search mod_delta =
   if mod_delta then my_find_search_delta
@@ -821,28 +825,31 @@ and my_find_search mod_delta =
     
 and my_find_search_delta db_list local_db hdc concl =
   let flags = {auto_unif_flags with use_metas_eagerly = true} in
+  let f = hintmap_of hdc concl in
     if occur_existential concl then 
       list_map_append
 	(fun db -> 
 	  if Hint_db.use_dn db then 
 	    let flags = flags_of_state (Hint_db.transparent_state db) in
-	      List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	      List.map (fun x -> (Some flags,x)) (f db)
 	  else
 	    let flags = {flags with modulo_delta = Hint_db.transparent_state db} in
-	      List.map (fun x -> (Some flags,x)) (Hint_db.map_all hdc db))
+	      List.map (fun x -> (Some flags,x)) (f db))
 	(local_db::db_list)
     else
       list_map_append (fun db -> 
 	if Hint_db.use_dn db then 
 	  let flags = flags_of_state (Hint_db.transparent_state db) in
-	    List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	    List.map (fun x -> (Some flags, x)) (f db)
 	else
 	  let (ids, csts as st) = Hint_db.transparent_state db in
 	  let flags, l =
 	    let l =
-	      if (Idpred.is_empty ids && Cpred.is_empty csts)
-	      then Hint_db.map_auto (hdc,concl) db
-	      else Hint_db.map_all hdc db
+	      match hdc with None -> Hint_db.map_none db
+	      | Some hdc ->
+		  if (Idpred.is_empty ids && Cpred.is_empty csts)
+		  then Hint_db.map_auto (hdc,concl) db
+		  else Hint_db.map_all hdc db
 	    in {flags with modulo_delta = st}, l
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
@@ -861,13 +868,15 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
       
 and trivial_resolve mod_delta db_list local_db cl = 
   try 
-    let hdconstr,_ = head_constr_bound cl in
-    List.map (tac_of_hint db_list local_db cl)
-      (priority 
-	(my_find_search mod_delta db_list local_db
-	  (head_of_constr_reference hdconstr) cl))
-  with Bound | Not_found -> 
-    []
+    let head = 
+      try let hdconstr,_ = head_constr_bound cl in
+	    Some (head_of_constr_reference hdconstr)
+      with Bound -> None
+    in
+      List.map (tac_of_hint db_list local_db cl)
+	(priority 
+	    (my_find_search mod_delta db_list local_db head cl))
+  with Not_found -> []
 
 let trivial lems dbnames gl =
   let db_list = 
@@ -903,12 +912,14 @@ let h_trivial lems l =
 
 let possible_resolve mod_delta db_list local_db cl =
   try 
-    let hdconstr,_ = head_constr_bound cl in
-    List.map (tac_of_hint db_list local_db cl)
-      (my_find_search mod_delta db_list local_db
-        (head_of_constr_reference hdconstr) cl)
-  with Bound | Not_found -> 
-    []
+    let head = 
+      try let hdconstr,_ = head_constr_bound cl in
+	    Some (head_of_constr_reference hdconstr)
+      with Bound -> None
+    in
+      List.map (tac_of_hint db_list local_db cl)
+	(my_find_search mod_delta db_list local_db head cl)
+  with Not_found -> []
 
 let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
   try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c9065ef3..132b9063 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: auto.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id: auto.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -53,6 +53,7 @@ module Hint_db :
     type t
     val empty : transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
+    val map_none : t -> pri_auto_tactic list
     val map_all : global_reference -> t -> pri_auto_tactic list
     val map_auto : global_reference * constr -> t -> pri_auto_tactic list
     val add_one : hint_entry -> t -> t
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6a425984..b7eb3620 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -9,7 +9,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: class_tactics.ml4 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: class_tactics.ml4 12189 2009-06-15 05:08:44Z msozeau $ *)
 
 open Pp
 open Util
@@ -46,18 +46,18 @@ let typeclasses_db = "typeclass_instances"
 let _ = Auto.auto_init := (fun () -> 
   Auto.create_hint_db false typeclasses_db full_transparent_state true)
 
-let check_imported_library d =
+let check_required_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
   if not (Library.library_is_loaded dir) then
-    error ("Library "^(list_last d)^" has to be imported first.")
+    error ("Library "^(list_last d)^" has to be required first.")
       
 let classes_dirpath =
   make_dirpath (List.map id_of_string ["Classes";"Coq"])
   
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
-  else check_imported_library ["Coq";"Setoids";"Setoid"]
+  else check_required_library ["Coq";"Setoids";"Setoid"]
 
 (** Typeclasses instance search tactic / eauto *)
 
@@ -245,7 +245,6 @@ module SearchProblem = struct
 	    Option.iter (fun r ->
 (*  	      msg (str"do cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *)
 	      r := true) do_cut;
-	  let sigma = Evarutil.nf_evars sigma in
 	  let gl = List.map (Evarutil.nf_evar_info sigma) gl in
 	  let nbgl = List.length gl in
 (* 	  let gl' = { it = gl ; sigma = sigma } in *)
@@ -338,6 +337,7 @@ let is_transparent_gr (ids, csts) = function
   | IndRef _ | ConstructRef _ -> false
 
 let make_resolve_hyp env sigma st flags pri (id, _, cty) =
+  let cty = Evarutil.nf_evar sigma cty in
   let ctx, ar = decompose_prod cty in
   let keep = 
     match kind_of_term (fst (decompose_app ar)) with
@@ -625,9 +625,6 @@ let is_applied_setoid_relation t =
 let _ = 
   Equality.register_is_applied_setoid_relation is_applied_setoid_relation
 
-exception Found of (constr * constr * (types * types) list * constr * constr array *
-		       (constr * (constr * constr * constr * constr)) option array)
-
 let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
@@ -1675,7 +1672,7 @@ let typeclass_app_constrexpr t ?(bindings=NoBindings) gl =
   let bindings = Tacinterp.interp_bindings my_ist gl bl in
     typeclass_app (Evd.evars_of !evars) gl ~bindings:bindings j.uj_val j.uj_type
 
-let typeclass_app_raw t gl =
+let typeclass_app_raw (_,t) gl =
   let env = pf_env gl in
   let evars = ref (create_evar_defs (project gl)) in
   let j = Pretyping.Default.understand_judgment_tcc evars env t in
@@ -1715,7 +1712,7 @@ END
 
 let not_declared env ty rel =
   tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ 
-		str ty ++ str" relation. Maybe you need to import the Setoid library")
+		str ty ++ str" relation. Maybe you need to require the Setoid library")
 
 let relation_of_constr env c = 
   match kind_of_term c with
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 2d0395a3..62a8ddfc 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_proof_instr.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *)
 
 open Util
 open Pp
@@ -174,7 +174,7 @@ let mark_proof_tree_as_done pt =
 let mark_as_done pts = 
   map_pftreestate 
     (fun _ -> mark_proof_tree_as_done) 
-    (traverse 0 pts) 
+    (up_to_matching_rule is_focussing_command pts) 
 
 (* post-instruction focus management *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index baebee07..58a00419 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
 
 open Pp
 open Util
@@ -1215,7 +1215,7 @@ let subst_one x gl =
        tclMAP introtac depdecls]) @
      [tclTRY (clear [x;hyp])]) gl
 
-let subst = tclMAP subst_one
+let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
 
 let subst_all gl =
   let test (_,c) =
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 43c18a8b..67b89888 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_tactics.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: evar_tactics.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Term
 open Util
@@ -29,7 +29,7 @@ let evar_list evc c =
   in 
     evrec [] c
 
-let instantiate n rawc ido gl = 
+let instantiate n (ist,rawc) ido gl = 
   let sigma = gl.sigma in
   let evl = 
     match ido with
@@ -52,7 +52,9 @@ let instantiate n rawc ido gl =
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "Incorrect existential variable index.";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in
+    let env = Evd.evar_env (Evd.find sigma ev) in
+    let ltac_vars = Tacinterp.extract_ltac_vars ist sigma env in
+    let evd' = w_refine ev (ltac_vars,rawc) (create_goal_evar_defs sigma) in
       tclTHEN
         (tclEVARS (evars_of evd'))
         tclNORMEVAR
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index cc06d2c6..f577b338 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evar_tactics.mli 11512 2008-10-27 12:28:36Z herbelin $ i*)
+(*i $Id: evar_tactics.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 open Tacmach
 open Names
 open Tacexpr
 open Termops
 
-val instantiate : int -> Rawterm.rawconstr -> 
+val instantiate : int -> Tacinterp.interp_sign * Rawterm.rawconstr -> 
   (identifier * hyp_location_flag, unit) location -> tactic
 
 (*i
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 694c3495..5eb333a0 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extraargs.ml4 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: extraargs.ml4 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -100,9 +100,9 @@ END
 
 let pr_gen prc _prlc _prtac c = prc c
 
-let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw
+let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_rawconstr raw
 
-let interp_raw _ _ (t,_) = t
+let interp_raw ist gl (t,_) = (ist,t)
 
 let glob_raw = Tacinterp.intern_constr
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index bccb150f..b64adf24 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraargs.mli 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: extraargs.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 open Tacexpr
 open Term
@@ -25,7 +25,7 @@ val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
 val wit_occurrences : (int list) typed_abstract_argument_type
 
 val rawwit_raw : constr_expr raw_abstract_argument_type
-val wit_raw : rawconstr typed_abstract_argument_type
+val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type
 val raw : constr_expr Pcoq.Gram.Entry.e
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b270ba2d..8e517453 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: hiddentac.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Term
 open Proof_type
@@ -75,10 +75,6 @@ let h_generalize_dep c =
 let h_let_tac b na c cl =
   let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
   abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl)
-let h_instantiate n c ido = 
-(Evar_tactics.instantiate n c ido)
-  (* abstract_tactic (TacInstantiate (n,c,cls))
-    (Evar_refiner.instantiate n c (simple_clause_of cls)) *)
 
 (* Derived basic tactics *)
 let h_simple_induction_destruct isrec h =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 0ebb024a..9270411a 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hiddentac.mli 11671 2008-12-12 12:43:03Z herbelin $ i*)
+(*i $Id: hiddentac.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -62,8 +62,6 @@ val h_generalize_gen  : (constr with_occurrences * name) list -> tactic
 val h_generalize_dep  : constr -> tactic 
 val h_let_tac         : letin_flag -> name -> constr -> 
                         Tacticals.clause -> tactic
-val h_instantiate     : int -> Rawterm.rawconstr ->
-  (identifier * hyp_location_flag, unit) location -> tactic
 
 (* Derived basic tactics *)
 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index dff3b003..322d25e5 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refine.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (* JCF -- 6 janvier 1998  EXPERIMENTAL *)
 
@@ -327,29 +327,31 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
           gl
 
     (* fix => tactique Fix *)
-    | Fix ((ni,_),(fi,ai,_)) , _ ->
+    | Fix ((ni,j),(fi,ai,_)) , _ ->
 	let out_name = function
 	  | Name id -> id
           | _ -> error "Recursive functions must have names."
 	in
 	let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
+	let firsts,lasts = list_chop j (Array.to_list fixes) in
 	tclTHENS
-	  (mutual_fix (out_name fi.(0)) (succ ni.(0))
-	    (List.tl (Array.to_list fixes)))
+	  (mutual_fix_with_index 
+	    (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
 		       | None -> tclIDTAC 
 		       | Some th -> tcc_aux subst th) sgp)
 	  gl
 
     (* cofix => tactique CoFix *)
-    | CoFix (_,(fi,ai,_)) , _ ->
+    | CoFix (j,(fi,ai,_)) , _ ->
 	let out_name = function
 	  | Name id -> id
           | _ -> error "Recursive functions must have names."
 	in
 	let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
+	let firsts,lasts = list_chop j (Array.to_list cofixes) in
 	tclTHENS
-	  (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes)))
+	  (mutual_cofix_with_index (out_name fi.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
 		       | None -> tclIDTAC 
 		       | Some th -> tcc_aux subst th) sgp)
@@ -366,10 +368,15 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 
 (* Et finalement la tactique refine elle-même : *)
 
-let refine oc gl =
+let refine (evd,c) gl =
   let sigma = project gl in
-  let (sigma,c) = Evarutil.evars_to_metas sigma oc in
+  let evd = Evd.evars_of (Typeclasses.resolve_typeclasses
+			     ~onlyargs:true ~fail:false (pf_env gl) 
+			     (Evd.create_evar_defs evd)) 
+  in
+  let c = Evarutil.nf_evar evd c in
+  let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
   (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise 
      complicated to update meta types when passing through a binder *)
-  let th = compute_metamap (pf_env gl) sigma c in
-  tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl
+  let th = compute_metamap (pf_env gl) evd c in
+  tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d9026a6d..71b50b66 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Constrintern
 open Closure
@@ -539,7 +539,9 @@ let intern_induction_arg ist = function
   | ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))),NoBindings)
+	match intern_constr ist (CRef (Ident (dloc,id))) with
+	| RVar (loc,id),_ -> ElimOnIdent (loc,id)
+	| c -> ElimOnConstr (c,NoBindings)
       else
 	ElimOnIdent (loc,id)
 
@@ -1396,6 +1398,14 @@ let retype_list sigma env lst =
     try (x,Retyping.get_judgment_of env sigma csr)::a with
     | Anomaly _ -> a) lst []
 
+let extract_ltac_vars_data ist sigma env =
+  let (ltacvars,_ as vars) = constr_list ist env in
+  vars, retype_list sigma env ltacvars
+
+let extract_ltac_vars ist sigma env =
+  let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in
+  typs,unbndltacvars
+
 let implicit_tactic = ref None
 
 let declare_implicit_tactic tac = implicit_tactic := Some tac
@@ -1441,8 +1451,8 @@ let solve_remaining_evars env initial_sigma evd c =
   proc_rec (Evarutil.nf_isevar !evdref c)
 
 let interp_gen kind ist sigma env (c,ce) =
-  let (ltacvars,unbndltacvars as vars) = constr_list ist env in
-  let typs = retype_list sigma env ltacvars in
+  let (ltacvars,unbndltacvars as vars),typs =
+    extract_ltac_vars_data ist sigma env in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
@@ -1717,10 +1727,20 @@ let interp_induction_arg ist gl = function
   | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
   | ElimOnAnonHyp n as x -> x
   | ElimOnIdent (loc,id) ->
-      if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
-      else ElimOnConstr
-	(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
-	 NoBindings)
+      try
+	match List.assoc id ist.lfun with
+	| VInteger n -> ElimOnAnonHyp n
+	| VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id)
+	| VConstr c -> ElimOnConstr (c,NoBindings)
+	| _ -> user_err_loc (loc,"",
+	      strbrk "Cannot coerce " ++ pr_id id ++
+	      strbrk " neither to a quantified hypothesis nor to a term.")
+      with Not_found ->
+	(* Interactive mode *)
+	if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+	else ElimOnConstr
+	  (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
+	  NoBindings)
 
 let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
 let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
@@ -2735,6 +2755,7 @@ let bad_tactic_args s =
 
 (* Declaration of the TAC-DEFINITION object *)
 let add (kn,td) = mactab := Gmap.add kn td !mactab
+let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
 
 type tacdef_kind = | NewTac of identifier
 		   | UpdateTac of ltac_constant
@@ -2749,9 +2770,7 @@ let load_md i ((sp,kn),defs) =
 	  let kn = Names.make_kn mp dir (label_of_id id) in
 	    Nametab.push_tactic (Until i) sp kn;
 	    add (kn,t)
-      | UpdateTac kn ->
-	  mactab := Gmap.remove kn !mactab;
-	  add (kn,t)) defs
+      | UpdateTac kn -> replace (kn,t)) defs
     
 let open_md i((sp,kn),defs) =
   let dp,_ = repr_path sp in
@@ -2762,10 +2781,7 @@ let open_md i((sp,kn),defs) =
 	  let sp = Libnames.make_path dp id in
 	  let kn = Names.make_kn mp dir (label_of_id id) in
 	    Nametab.push_tactic (Exactly i) sp kn
-      | UpdateTac kn -> 
-	  let (path, id) = decode_kn kn in
-	  let sp = Libnames.make_path path id in
-	  Nametab.push_tactic (Exactly i) sp kn) defs
+      | UpdateTac kn -> ()) defs
 
 let cache_md x = load_md 1 x
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index add57cb5..b66bdb85 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacinterp.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: tacinterp.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 (*i*)
 open Dyn
@@ -44,6 +44,9 @@ and interp_sign =
     debug : debug_info;
     trace : ltac_trace }
 
+val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env -> 
+  Pretyping.var_map * Pretyping.unbound_ltac_var_map
+
 (* Transforms an id into a constr if possible *)
 val constr_of_id : Environ.env -> identifier -> constr
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 28e987fa..3db6bcef 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacticals.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
+(* $Id: tacticals.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Pp
 open Util
@@ -26,7 +26,6 @@ open Clenvtac
 open Rawterm
 open Pattern
 open Matching
-open Evar_refiner
 open Genarg
 open Tacexpr
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2c567034..0a8b5d01 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -155,19 +155,37 @@ let order_hyps      = Tacmach.order_hyps
 (* Renaming hypotheses *)
 let rename_hyp      = Tacmach.rename_hyp
 
+(**************************************************************)
+(*          Fresh names                                       *)
+(**************************************************************)
+
+let fresh_id_avoid avoid id =
+  next_global_ident_away true id avoid
+
+let fresh_id avoid id gl =
+  fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
+
+(**************************************************************)
+(*          Fixpoints and CoFixpoints                         *)
+(**************************************************************)
+
 (* Refine as a fixpoint *)
 let mutual_fix = Tacmach.mutual_fix
 
-let fix ido n = match ido with
-  | None -> mutual_fix (Pfedit.get_current_proof_name ()) n []
-  | Some id -> mutual_fix id n []
+let fix ido n gl = match ido with
+  | None -> 
+      mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] gl
+  | Some id ->
+      mutual_fix id n [] gl
 
 (* Refine as a cofixpoint *)
 let mutual_cofix = Tacmach.mutual_cofix
 
-let cofix = function
-  | None -> mutual_cofix (Pfedit.get_current_proof_name ()) []
-  | Some id -> mutual_cofix id []
+let cofix ido gl = match ido with
+  | None -> 
+      mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] gl
+  | Some id ->
+      mutual_cofix id [] gl
 
 (**************************************************************)
 (*          Reduction and conversion tactics                  *)
@@ -286,12 +304,6 @@ let unfold_constr = function
 (*         Introduction tactics            *)
 (*******************************************)
 
-let fresh_id_avoid avoid id =
-  next_global_ident_away true id avoid
-
-let fresh_id avoid id gl =
-  fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
-
 let id_of_name_with_default id = function
   | Anonymous -> id
   | Name id   -> id
@@ -565,9 +577,14 @@ let error_uninstantiated_metas t clenv =
   let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
   in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
-let clenv_refine_in with_evars id clenv gl =
+let clenv_refine_in with_evars ?(with_classes=true) id clenv gl =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
-  let new_hyp_typ  = clenv_type clenv in
+  let clenv = 
+    if with_classes then 
+      { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd }
+    else clenv
+  in
+  let new_hyp_typ = clenv_type clenv in
   if not with_evars & occur_meta new_hyp_typ then 
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf  = clenv_value clenv in
@@ -1098,9 +1115,6 @@ let forward_general_multi_rewrite =
 let register_general_multi_rewrite f =
   forward_general_multi_rewrite := f
 
-let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
-let case_last  = tclLAST_HYP simplest_case
-
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
   | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
@@ -1111,8 +1125,8 @@ let error_unexpected_extra_pattern loc nb pat =
        str (if nb = 1 then "was" else "were") ++
       strbrk " expected in the branch).")
 
-let intro_or_and_pattern loc b ll l' tac =
-  tclLAST_HYP (fun c gl ->
+let intro_or_and_pattern loc b ll l' tac id gl =
+    let c = mkVar id in
     let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
     let nv = mis_constr_nargs ind in
     let bracketed = b or not (l'=[]) in
@@ -1126,10 +1140,10 @@ let intro_or_and_pattern loc b ll l' tac =
     let ll = fix_empty_or_and_pattern (Array.length nv) ll in
     check_or_and_pattern_size loc ll (Array.length nv);
     tclTHENLASTn
-      (tclTHEN case_last clear_last)
+      (tclTHEN (simplest_case c) (clear [id]))
       (array_map2 (fun n l -> tac ((adjust_names_length n n l)@l'))
 	nv (Array.of_list ll))
-      gl)
+      gl
 
 let rewrite_hyp l2r id gl =
   let rew_on l2r =
@@ -1194,8 +1208,9 @@ let rec intros_patterns b avoid thin destopt = function
   | (loc, IntroOrAndPattern ll) :: l' ->
       tclTHEN
         introf
-        (intro_or_and_pattern loc b ll l'
-	  (intros_patterns b avoid thin destopt))
+        (onLastHyp
+	  (intro_or_and_pattern loc b ll l'
+	    (intros_patterns b avoid thin destopt)))
   | (loc, IntroRewrite l2r) :: l ->
       tclTHEN 
         (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
@@ -1229,8 +1244,10 @@ let prepare_intros s ipat gl = match ipat with
   | IntroRewrite l2r -> 
       let id = make_id s gl in
       id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
-  | IntroOrAndPattern ll -> make_id s gl, 
-      intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
+  | IntroOrAndPattern ll -> make_id s gl,
+      onLastHyp
+	(intro_or_and_pattern loc true ll [] 
+	  (intros_patterns true [] [] no_move))
 
 let ipat_of_name = function
   | Anonymous -> None
@@ -1261,6 +1278,7 @@ let as_tac id ipat = match ipat with
       !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
   | Some (loc,IntroOrAndPattern ll) ->
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
+        id
   | Some (loc,
       (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) ->
       user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
@@ -2167,7 +2185,7 @@ let dependent_pattern c gl =
     let conclvar = subst_term_occ all_occurrences c ty in
       mkNamedLambda id cty conclvar
   in
-  let subst = (c, varname c, cty) :: List.map (fun c -> (c, varname c, pf_type_of gl c)) deps in
+  let subst = (c, varname c, cty) :: List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in
   let concllda = List.fold_left mklambda (pf_concl gl) subst in 
   let conclapp = applistc concllda (List.rev_map pi1 subst) in
     convert_concl_no_check conclapp DEFAULTcast gl
diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v
index bd7fd796..fb2725c9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1905.v
+++ b/test-suite/bugs/closed/shouldsucceed/1905.v
@@ -1,5 +1,5 @@
 
-Require Import Setoid.
+Require Import Setoid Program.
 
 Axiom t : Set.
 Axiom In : nat -> t -> Prop.
diff --git a/test-suite/bugs/closed/shouldsucceed/2089.v b/test-suite/bugs/closed/shouldsucceed/2089.v
new file mode 100644
index 00000000..aebccc94
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2089.v
@@ -0,0 +1,17 @@
+Inductive even (x: nat): nat -> Prop :=
+  | even_base: even x O
+  | even_succ: forall n, odd x n -> even x (S n)
+
+with odd (x: nat): nat -> Prop :=
+  | odd_succ: forall n, even x n -> odd x (S n).
+
+Scheme even_ind2 := Minimality for even Sort Prop
+  with odd_ind2 := Minimality for odd Sort Prop.
+
+Combined Scheme even_odd_ind from even_ind2, odd_ind2.
+
+Check (even_odd_ind :forall (x : nat) (P P0 : nat -> Prop),
+  P 0 ->
+  (forall n : nat, odd x n -> P0 n -> P (S n)) ->
+  (forall n : nat, even x n -> P n -> P0 (S n)) ->
+  (forall n : nat, even x n -> P n) /\ (forall n : nat, odd x n -> P0 n)).
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 488b057f..46dd0cb6 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,5 +1,4 @@
 Require Import Coq.Program.Program.
-Set Manual Implicit Arguments.
 
 
 Variable A : Set.
@@ -105,7 +104,7 @@ Save.
 
 (** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *)
 
-Unset Manual Implicit Arguments.
+Set Implicit Arguments.
 
 Inductive Ty :=
  | Nat : Ty
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 157217ae..15cabf81 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -12,9 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: EquivDec.v 11800 2009-01-18 18:34:15Z msozeau $ *)
-
-Set Manual Implicit Arguments.
+(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Export notations. *)
 
@@ -144,9 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
       | _, _ => in_right
     end }.
 
-  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
+  Solve Obligations using unfold equiv, complement in *; program_simpl;
+    intuition (discriminate || eauto).
 
-  Next Obligation.
-  Proof. clear aux. red in H0. subst. 
-    destruct y; intuition (discriminate || eauto).
-  Defined.
+  Next Obligation. destruct x ; destruct y ; intuition eauto. Defined.
+
+  Solve Obligations using unfold equiv, complement in *; program_simpl;
+    intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 5e5895ab..7068bc6b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -12,15 +12,15 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *) 
 
-(* $Id: Equivalence.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
-Require Export Coq.Program.Basics.
+Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
 Require Import Coq.Classes.Init.
 Require Import Relation_Definitions.
-Require Import Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 5df7a4ed..762cc5c1 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,12 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Init.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-(* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
-
-Tactic Notation "clapply" ident(c) :=
-  eapply @c ; typeclasses eauto.
+(* $Id: Init.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Hints for the proof search: these combinators should be considered rigid. *)
 
@@ -29,12 +24,12 @@ Typeclasses Opaque id const flip compose arrow impl iff.
 (** The unconvertible typeclass, to test that two objects of the same type are 
    actually different. *)
 
-Class Unconvertible (A : Type) (a b : A).
+Class Unconvertible (A : Type) (a b : A) := unconvertible : unit.
 
 Ltac unconvertible :=
   match goal with
     | |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible"
-    | |- _ => eapply Build_Unconvertible 
+    | |- _ => exact tt
   end.
 
 Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 86097a56..2b653e27 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -13,9 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Morphisms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-Set Manual Implicit Arguments.
+(* $Id: Morphisms.v 12189 2009-06-15 05:08:44Z msozeau $ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
@@ -55,18 +52,24 @@ Definition respectful {A B : Type}
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
 Delimit Scope signature_scope with signature.
+
 Arguments Scope Morphism [type_scope signature_scope].
+Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
 
-Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
-  (right associativity, at level 55) : signature_scope.
+Module MorphismNotations.
 
-Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
+  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
+    (right associativity, at level 55) : signature_scope.
+  
+  Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+  
+  Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
 
-Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
+End MorphismNotations.
 
-Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
+Export MorphismNotations.
 
 Open Local Scope signature_scope.
 
@@ -118,7 +121,7 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
 (** And of course it is reflexive. *)
 
-Instance morphisms_subrelation_refl : ! subrelation A R R | 10.
+Instance morphisms_subrelation_refl : ! subrelation A R R.
 Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
@@ -151,10 +154,10 @@ Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
-Instance iff_impl_subrelation : subrelation iff impl.
+Instance iff_impl_subrelation : subrelation iff impl | 2.
 Proof. firstorder. Qed.
 
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.
 Proof. firstorder. Qed.
 
 Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
@@ -372,25 +375,6 @@ Ltac partial_application_tactic :=
       end
   end.
 
-Section PartialAppTest.
-  Instance and_ar : Params and 0.
-
-  Goal Morphism (iff) (and True True).
-    partial_application_tactic.
-  Admitted.
-
-  Goal Morphism (iff) (or True True).
-    partial_application_tactic.
-    partial_application_tactic. 
-  Admitted.
-
-  Goal Morphism (iff ==> iff) (iff True).
-    partial_application_tactic.
-    (*partial_application_tactic. *)
-   Admitted.
-
-End PartialAppTest.
-
 Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 24b8d636..4654e654 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -12,6 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
+Require Import Relation_Definitions.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Program.
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index f95894be..e1de9ee9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -13,12 +13,12 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: RelationClasses.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
 
 (** We allow to unfold the [relation] definition while doing morphism search. *)
 
@@ -368,7 +368,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
    We give an equivalent definition, up-to an equivalence relation 
    on the carrier. *)
 
-Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
@@ -377,7 +377,8 @@ Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
 
 Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. 
+  reduce_goal. 
+  pose proof partial_order_equivalence as poe. do 3 red in poe. 
   apply <- poe. firstorder.
 Qed.
 
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index 305168ec..03bb9a80 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -12,7 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidAxioms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *)
 
 Require Import Coq.Program.Program.
 
@@ -22,7 +22,7 @@ Unset Strict Implicit.
 Require Export Coq.Classes.SetoidClass.
 
 (* Application of the extensionality axiom to turn a goal on 
-   Leibinz equality to a setoid equivalence (use with care!). *)
+   Leibniz equality to a setoid equivalence (use with care!). *)
 
 Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 47f92ada..d3da7d5a 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -12,14 +12,14 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: SetoidClass.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: SetoidClass.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 Require Import Coq.Program.Program.
 
-Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
 Require Import Coq.Classes.Functions.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index caacc9ec..36f05e31 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -13,13 +13,13 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidTactics.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: SetoidTactics.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
-Require Export Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
-Require Export Coq.Classes.Morphisms_Prop.
-Require Export Coq.Classes.Equivalence.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Equivalence Coq.Program.Basics.
+
+Export MorphismNotations.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index df12166e..d91eb87a 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FMapFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *)
+(* $Id: FMapFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** * Finite maps library *)
 
@@ -15,7 +15,7 @@
   different styles: equivalence and boolean equalities. 
 *)
 
-Require Import Bool DecidableType DecidableTypeEx OrderedType.
+Require Import Bool DecidableType DecidableTypeEx OrderedType Morphisms.
 Require Export FMapInterface. 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 1e15d3a1..674caaac 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FSetFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *)
+(* $Id: FSetFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** * Finite sets library *)
 
@@ -17,7 +17,7 @@
 *)
 
 Require Import DecidableTypeEx.
-Require Export FSetInterface. 
+Require Export FSetInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -424,14 +424,14 @@ Add Relation t Subset
  transitivity proved by Subset_trans
  as SubsetSetoid.
 
-Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1.
+Instance In_s_m : Morphisms.Morphism (E.eq ==> Subset ++> Basics.impl) In | 1.
 Proof.
   simpl_relation. eauto with set.
 Qed.
 
-Add Morphism Empty with signature Subset --> impl as Empty_s_m.
+Add Morphism Empty with signature Subset --> Basics.impl as Empty_s_m.
 Proof.
-unfold Subset, Empty, impl; firstorder.
+unfold Subset, Empty, Basics.impl; firstorder.
 Qed.
 
 Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 3753b97b..ff70c9fb 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ConstructiveEpsilon.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
+(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*)
 
 (** This module proves the constructive description schema, which
 infers the sigma-existence (i.e., [Set]-existence) of a witness to a
@@ -14,8 +14,8 @@ predicate from the regular existence (i.e., [Prop]-existence). One
 requires that the underlying set is countable and that the predicate
 is decidable. *)
 
-(** Coq does not allow case analysis on sort [Set] when the goal is in
-[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
+(** Coq does not allow case analysis on sort [Prop] when the goal is in
+[Set]. Therefore, one cannot eliminate [exists n, P n] in order to
 show [{n : nat | P n}]. However, one can perform a recursion on an
 inductive predicate in sort [Prop] so that the returning type of the
 recursion is in [Set]. This trick is described in Coq'Art book, Sect.
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index 4445b0e1..0dc82907 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -11,8 +11,6 @@
 (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
    It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *)
 
-Set Manual Implicit Arguments.
-
 (** The converse of functional extensionality. *)
 
 Lemma equal_f : forall {A B : Type} {f g : A -> B}, 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 99d54755..9681d543 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Equality.v 11709 2008-12-20 11:42:15Z msozeau $ i*)
+(*i $Id: Equality.v 12073 2009-04-08 21:04:42Z msozeau $ i*)
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
@@ -479,8 +479,12 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac do_case p := destruct p || elim_case p || (case p ; clear p).
-Ltac do_ind p := induction p || elim_ind p.
+Ltac introduce p := 
+  first [ match p with _ => idtac end (* Already there *)
+    | intros until p | intros ].
+
+Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
+Ltac do_ind p := introduce p ; (induction p || elim_ind p).
 
 Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 12bdf3a7..2083e530 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: Wf.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Wf.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Reformulation of the Wf module using subsets where possible, providing
    the support for [Program]'s treatment of well-founded definitions. *)
@@ -165,7 +165,7 @@ Section Measure_well_founded.
 
   (* Measure relations are well-founded if the underlying relation is well-founded. *)
 
-  Variables T M: Set.
+  Variables T M: Type.
   Variable R: M -> M -> Prop.
   Hypothesis wf: well_founded R.
   Variable m: T -> M.
@@ -191,7 +191,7 @@ End Measure_well_founded.
 
 Section Fix_measure_rects.
 
-  Variable A: Set.
+  Variable A: Type.
   Variable m: A -> nat.
   Variable P: A -> Type.
   Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x.
@@ -287,7 +287,7 @@ Section Fix_measure_rects.
 
 End Fix_measure_rects.
 
-(** Tactic to fold a definitions based on [Fix_measure_sub]. *)
+(** Tactic to fold a definition based on [Fix_measure_sub]. *)
 
 Ltac fold_sub f :=
   match goal with
@@ -312,8 +312,8 @@ Module WfExtensionality.
   (** For a function defined with Program using a well-founded order. *)
 
   Program Lemma fix_sub_eq_ext :
-    forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
-      (P : A -> Set)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
       (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
       forall x : A,
         Fix_sub A R Rwf P F_sub x =
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index e7fe82b2..a187a7c6 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -6,10 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Setoid.v 11720 2008-12-28 07:12:15Z letouzey $: i*)
+(*i $Id: Setoid.v 12187 2009-06-13 19:36:59Z msozeau $: i*)
 
 Require Export Coq.Classes.SetoidTactics.
 
+Export Morphisms.MorphismNotations.
+
 (** For backward compatibility *)
 
 Definition Setoid_Theory := @Equivalence.
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 98457261..eb3a19fa 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_makefile.ml4 11883 2009-02-06 09:54:52Z herbelin $ *)
+(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -212,7 +212,7 @@ let clean sds sps =
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
          $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n";
   if !some_mlfile then
-    print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n";
+    print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)\n";
   if Coq_config.has_natdynlink && !some_mlfile then
     print "\trm -f $(CMXSFILES) $(CMXSFILES:.cmxs=.o)\n";
   print "\t- rm -rf html\n";
@@ -243,14 +243,14 @@ let footer_includes () =
 let implicit () =
   let ml_rules () =
     print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
-    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
-    print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
+    print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+    print "%.cmxs: %.ml\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
     print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
-    print "%.cmxs: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
+    print "%.cmxs: %.ml4\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
     print "%.ml.d: %.ml\n";
-    print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n"
+    print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(OCAMLLIBS) $(PP) \"$<\" > \"$@\"\n\n"
   and v_rule () =
     print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n";
     print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -283,8 +283,8 @@ let variables defs =
     print "COQDOC:=$(COQBIN)coqdoc\n";
     print "COQMKTOP:=$(COQBIN)coqmktop\n";
     (* Caml executables and relative variables *)
-    printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
-    printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
+    printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc;
+    printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt;
     printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
     printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
     print "GRAMMARS:=grammar.cma\n";
@@ -315,7 +315,7 @@ let include_dirs (inc_i,inc_r) =
   let str_i' = parse_includes inc_i' in
   let str_r = parse_rec_includes inc_r in
     section "Libraries definitions.";
-    print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n  " str_i; print "\n";
+    print "OCAMLLIBS:="; print_list "\\\n  " str_i; print "\n";
     print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\
   -I $(COQLIB)/library -I $(COQLIB)/parsing \\
   -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5bcbed64..b3f0739d 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -54,9 +54,10 @@ let toc = ref false
 let page_title = ref ""
 let title = ref ""
 let externals = ref true
-let coqlib = ref "http://coq.inria.fr/library/"
+let coqlib = ref Coq_config.wwwstdlib
 let coqlib_path = ref Coq_config.coqlib
 let raw_comments = ref false
+let parse_comments = ref false
 let interpolate = ref false
 
 let charset = ref "iso-8859-1"
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index a9a99706..762be5af 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -57,6 +57,11 @@ body { padding: 0px 0px;
     display: inline;
     font-family: monospace } 
 
+.comment { 
+    display: inline;
+    font-family: monospace;
+    color: red; } 
+
 .code { 
     display: block;
     font-family: monospace } 
@@ -80,18 +85,46 @@ body { padding: 0px 0px;
     color: rgb(40%,0%,40%);
 }
 
+.id[type="variable"] { 
+    color: rgb(40%,0%,40%);
+}
+
 .id[type="definition"] { 
     color: rgb(0%,40%,0%);
 }
 
+.id[type="abbreviation"] { 
+    color: rgb(0%,40%,0%);
+}
+
 .id[type="lemma"] { 
     color: rgb(0%,40%,0%);
 }
 
+.id[type="instance"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="projection"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="method"] { 
+    color: rgb(0%,40%,0%);
+}
+
 .id[type="inductive"] { 
     color: rgb(0%,0%,80%);
 }
 
+.id[type="record"] { 
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="class"] { 
+    color: rgb(0%,0%,80%);
+}
+
 .id[type="keyword"] { 
  color : #cf1d1d;
 /*     color: black; */
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index ef4f4119..fca9a1d7 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -70,6 +70,9 @@
 % !!! CAUTION: This environment may have empty contents
 \newenvironment{coqdoccode}{}{}
 
+% Environment for comments
+\newenvironment{coqdoccomment}{\tt(*}{*)}
+
 % newline and indentation 
 %BEGIN LATEX
 % Base indentation length
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2e97618b..2ee9ac96 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 11828 2009-01-22 06:44:11Z notin $ i*)
+(*i $Id: main.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -56,7 +56,7 @@ let usage () =
   prerr_endline "  --verbose            verbose mode";  
   prerr_endline "  --no-externals       no links to Coq standard library";
   prerr_endline "  --coqlib <url>       set URL for Coq standard library";
-  prerr_endline "                       (default is http://coq.inria.fr/library/)";
+  prerr_endline ("                       (default is " ^ Coq_config.wwwstdlib ^ ")");
   prerr_endline "  --boot               run in boot mode";
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
@@ -65,6 +65,7 @@ let usage () =
   prerr_endline "  --charset <string>   set HTML charset";
   prerr_endline "  --inputenc <string>  set LaTeX input encoding";
   prerr_endline "  --interpolate        try to typeset identifiers in comments using definitions in the same module";
+  prerr_endline "  --parse-comments     parse regular comments";
   prerr_endline "";
   exit 1
 
@@ -273,6 +274,8 @@ let parse () =
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
 	Cdglobals.raw_comments := true; parse_rec rem
+    | ("-parse-comments" | "--parse-comments") :: rem ->
+	Cdglobals.parse_comments := true; parse_rec rem
     | ("-interpolate" | "--interpolate") :: rem ->
 	Cdglobals.interpolate := true; parse_rec rem
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index c146150c..1ad8b14f 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*)
+(*i $Id: output.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 open Cdglobals
 open Index
@@ -292,13 +292,13 @@ module Latex = struct
 
   let ident s l = 
     if !in_title then (
-      printf "\\texorpdfstring{";
+      printf "\\texorpdfstring{\\protect";
       with_latex_printing (fun s -> ident s l) s;
       printf "}{"; raw_ident s; printf "}")
     else
       with_latex_printing (fun s -> ident s l) s
     
-  let symbol = with_latex_printing raw_ident
+  let symbol s = with_latex_printing raw_ident s
 
   let rec reach_item_level n = 
     if !item_level < n then begin
@@ -320,6 +320,12 @@ module Latex = struct
 
   let end_doc () = in_doc := false; stop_item ()
 
+  let comment c = char c
+
+  let start_comment () = printf "\\begin{coqdoccomment}\n"
+
+  let end_comment () = printf "\\end{coqdoccomment}\n"
+
   let start_coq () = printf "\\begin{coqdoccode}\n"
 
   let end_coq () = printf "\\end{coqdoccode}\n"
@@ -389,8 +395,6 @@ module Html = struct
 	  printf "<div id=\"main\">\n\n"
 	end
 
-  let self = "http://coq.inria.fr"
-
   let trailer () =
     if !index && !current_module <> "Index" then 
       printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
@@ -406,7 +410,7 @@ module Html = struct
       else
 	begin
 	  printf "<hr/>This page has been generated by ";
-	  printf "<a href=\"%s\">coqdoc</a>\n" self;
+	  printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
 	  printf "</div>\n\n</div>\n\n</body>\n</html>"
 	end
 
@@ -456,14 +460,15 @@ module Html = struct
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
 	printf "<span class=\"id\" type=\"%s\">" typ; 
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s;
-	printf "</a></span>"
+	raw_ident s;
+	printf "</span></a>"
     | Coqlib when !externals ->
 	let m = Filename.concat !coqlib m in
-	  printf "<span class=\"id\" type=\"%s\">" typ; 
 	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	  raw_ident s; printf "</a></span>"
+	  printf "<span class=\"id\" type=\"%s\">" typ; 
+	  raw_ident s; printf "</span></a>"
     | Coqlib | Unknown ->
 	printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
 	  
@@ -477,8 +482,9 @@ module Html = struct
 	try
 	  (match Index.find !current_module loc with
 	     | Def (fullid,ty) -> 
+		 printf "<a name=\"%s\">" fullid; 
 		 printf "<span class=\"id\" type=\"%s\">" (type_name ty); 
-		 printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>"
+		 raw_ident s; printf "</span></a>"
              | Mod (m,s') when s = s' ->
 		 module_ref m s
 	     | Ref (m,fullid,ty) -> 
@@ -500,9 +506,11 @@ module Html = struct
     with Not_found -> 
       f tok
 
-  let ident s l = with_html_printing (fun s -> ident s l) s
+  let ident s l =
+    with_html_printing (fun s -> ident s l) s
 
-  let symbol = with_html_printing raw_ident
+  let symbol s =
+    with_html_printing raw_ident s
 
   let rec reach_item_level n = 
     if !item_level < n then begin
@@ -532,6 +540,10 @@ module Html = struct
     stop_item (); 
     if not !raw_comments then printf "\n</div>\n"
 
+  let start_comment () = printf "<span class=\"comment\">(*"
+
+  let end_comment () = printf "*)</span>"
+
   let start_code () = end_doc (); start_coq ()
 
   let end_code () = end_coq (); start_doc ()
@@ -540,7 +552,11 @@ module Html = struct
 
   let end_inline_coq () = printf "</span>"
 
-  let paragraph () = stop_item (); printf "\n<br/><br/>\n"
+  let paragraph () = 
+    let i = !item_level in
+      stop_item ();
+      if i > 0 then printf "\n"
+      else printf "\n<br/> <br/>\n"
 
   let section lev f =
     let lab = new_label () in
@@ -770,6 +786,9 @@ module TeXmacs = struct
 
   let end_coq () = ()
 
+  let start_comment () = ()
+  let end_comment () = ()
+
   let start_code () = in_doc := true; printf "<\\code>\n"
   let end_code () = in_doc := false; printf "\n</code>"
 
@@ -849,7 +868,7 @@ module Raw = struct
 
   let ident s loc = raw_ident s
 
-  let symbol = raw_ident
+  let symbol s = raw_ident s
 
   let item n = printf "- "
 
@@ -858,6 +877,9 @@ module Raw = struct
   let start_doc () = printf "(** "
   let end_doc () = printf " *)\n"
 
+  let start_comment () = ()
+  let end_comment () = ()
+
   let start_coq () = ()
   let end_coq () = ()
 
@@ -911,6 +933,9 @@ let start_module =
 let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
 let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc
 
+let start_comment = select Latex.start_comment Html.start_comment TeXmacs.start_comment Raw.start_comment
+let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment Raw.end_comment
+
 let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq
 let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
 
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 3da80335..75c7ccf8 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: output.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 open Cdglobals
 open Index
@@ -28,6 +28,9 @@ val start_module : unit -> unit
 val start_doc : unit -> unit
 val end_doc : unit -> unit
 
+val start_comment : unit -> unit
+val end_comment : unit -> unit
+
 val start_coq : unit -> unit
 val end_coq : unit -> unit
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 3ae5cbed..c4a1a76f 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*)
+(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -57,7 +57,7 @@
   let formatted = ref false
   let brackets = ref 0
   let comment_level = ref 0
-  let in_proof = ref false
+  let in_proof = ref None
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
@@ -162,6 +162,8 @@
     else
       String.sub s 1 (String.length s - 3)
 
+  let symbol lexbuf s = Output.symbol s 
+
 }
 
 (*s Regular expressions *)
@@ -217,7 +219,10 @@ let thm_token =
   | "Proposition" 
   | "Property"
   | "Goal"
-  | "Next" space+ "Obligation"
+
+let prf_token =
+  "Next" space+ "Obligation"
+  | "Proof" (space* "." | space+ "with")
 
 let def_token = 
   "Definition" 
@@ -290,7 +295,7 @@ let commands =
   | ("Hypothesis" | "Hypotheses")
   | "End"
 
-let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
 
 let extraction = 
   "Extraction"
@@ -307,7 +312,6 @@ let prog_kw =
 
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
-  | "Next" "Obligation"
   | "Ltac"
   | "Require"
   | "Import"
@@ -343,7 +347,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 
 rule coq_bol = parse
   | space* nl+
-      { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf }
+      { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -379,27 +383,29 @@ rule coq_bol = parse
 	  Output.indentation nbsp;
 	  Output.ident s (lexeme_start lexbuf + isp); 
 	  let eol = body lexbuf in
-	    in_proof := true;
+	    in_proof := Some eol;
 	    if eol then coq_bol lexbuf else coq lexbuf }
-  | space* "Proof" (space* "." | space+ "with")
-      { in_proof := true;
+  | space* prf_token
+      { in_proof := Some true;
 	let eol = 
-	if not !Cdglobals.gallina then 
-	  begin backtrack lexbuf; body_bol lexbuf end 
-	else true
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; body_bol lexbuf end 
+	  else 
+	    let s = lexeme lexbuf in
+	      if s.[String.length s - 1] = '.' then false
+	      else skip_to_dot lexbuf
 	in if eol then coq_bol lexbuf else coq lexbuf }
   | space* end_kw { 
       let eol = 
-	if not (!in_proof && !Cdglobals.gallina) then 
+	if not (!in_proof <> None && !Cdglobals.gallina) then 
 	  begin backtrack lexbuf; body_bol lexbuf end 
-	else
-	  skip_to_dot lexbuf 
+	else skip_to_dot lexbuf
       in
-	in_proof := false;
+	in_proof := None;
 	if eol then coq_bol lexbuf else coq lexbuf }
   | space* gallina_kw
       { 
-	in_proof := false;
+	in_proof := None;
 	let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
 	let s = String.sub s isp (String.length s - isp)  in
@@ -409,7 +415,7 @@ rule coq_bol = parse
 	    if eol then coq_bol lexbuf else coq lexbuf }
   | space* prog_kw
       { 
-	in_proof := false;
+	in_proof := None;
 	let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
 	  Output.indentation nbsp;
@@ -441,6 +447,12 @@ rule coq_bol = parse
 	coq_bol lexbuf }
   | space* "(*"
       { comment_level := 1; 
+	if !Cdglobals.parse_comments then begin
+	  let s = lexeme lexbuf in 
+	  let nbsp,isp = count_spaces s in
+	    Output.indentation nbsp;
+	    Output.start_comment ();
+	end;
 	let eol = comment lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
@@ -458,7 +470,7 @@ rule coq_bol = parse
 
 and coq = parse
   | nl 
-      { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
+      { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -466,12 +478,18 @@ and coq = parse
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
       { comment_level := 1;
+	if !Cdglobals.parse_comments then begin
+	  let s = lexeme lexbuf in 
+	  let nbsp,isp = count_spaces s in
+	    Output.indentation nbsp;
+	    Output.start_comment ();
+	end;
 	let eol = comment lexbuf in
-	  if eol then begin Output.line_break(); coq_bol lexbuf end 
+	  if eol then coq_bol lexbuf
           else coq lexbuf
       }
   | nl+ space* "]]"
-      { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end }
+      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
   | eof 
       { () }
   | gallina_kw_to_hide
@@ -487,14 +505,29 @@ and coq = parse
 	      let eol=body lexbuf in 
 		if eol then coq_bol lexbuf else coq lexbuf
 	    end }
+  | prf_token
+      { let eol = 
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; body_bol lexbuf end 
+	  else 
+	    let s = lexeme lexbuf in
+	    let eol = 
+	      if s.[String.length s - 1] = '.' then false
+	      else skip_to_dot lexbuf
+	    in
+	      eol
+	in if eol then coq_bol lexbuf else coq lexbuf }
   | end_kw { 
       let eol = 
-	if not (!in_proof && !Cdglobals.gallina) then 
+	if not !Cdglobals.gallina then 
 	  begin backtrack lexbuf; body lexbuf end 
-	else
-	  skip_to_dot lexbuf 
+	else 
+	  let eol = skip_to_dot lexbuf in
+	    if !in_proof <> Some true && eol then 
+	      Output.line_break ();
+	    eol
       in
-	in_proof := false;
+	in_proof := None;
 	if eol then coq_bol lexbuf else coq lexbuf }
   | gallina_kw
       { let s = lexeme lexbuf in 
@@ -513,8 +546,7 @@ and coq = parse
 	  if not !Cdglobals.gallina then 
 	    begin backtrack lexbuf; body lexbuf end 
 	  else 
-	    let eol = skip_to_dot lexbuf in
-	      if eol then Output.line_break (); eol
+	    skip_to_dot lexbuf
 	in 
 	  if eol then coq_bol lexbuf else coq lexbuf}
       
@@ -616,8 +648,7 @@ and escaped_coq = parse
       { () }
   | token_brackets
       { let s = lexeme lexbuf in
-	Output.symbol s;
-	escaped_coq lexbuf }
+	  symbol lexbuf s; escaped_coq lexbuf }
   | (identifier '.')* identifier
       { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
   | _ 
@@ -644,15 +675,30 @@ and comments = parse
 (*s Skip comments *)
 
 and comment = parse
-  | "(*" { incr comment_level; comment lexbuf }
-  | "*)" space* nl { decr comment_level; if !comment_level > 0 then comment lexbuf else true }
-  | "*)" { decr comment_level; if !comment_level > 0 then comment lexbuf else false }
-  | eof  {  false }
-  | _    {  comment lexbuf }
-
+  | "(*" { incr comment_level;
+	   if !Cdglobals.parse_comments then Output.start_comment ();
+	   comment lexbuf }
+  | "*)" space* nl {
+      if !Cdglobals.parse_comments then	(Output.end_comment (); Output.line_break ());
+      decr comment_level; if !comment_level > 0 then comment lexbuf else true }
+  | "*)" { 
+      if !Cdglobals.parse_comments then (Output.end_comment ());
+      decr comment_level; if !comment_level > 0 then comment lexbuf else false }
+  | "[" { 
+      if !Cdglobals.parse_comments then (
+	brackets := 1;
+	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ());
+      comment lexbuf }
+  | eof  { false }
+  | space+ { if !Cdglobals.parse_comments then 
+	Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
+  | nl   { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
+  | _    { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
+  comment lexbuf }
+      
 and skip_to_dot = parse
   | '.' space* nl { true }
-  | eof | '.' space+ { false}
+  | eof | '.' space+ { false }
   | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
 
@@ -664,15 +710,19 @@ and body_bol = parse
 and body = parse
   | nl {Output.line_break(); body_bol lexbuf}
   | nl+ space* "]]"
-      { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true }
+      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
   | eof { false }
-  | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
-  | '.' space+ { Output.char '.'; Output.char ' '; false }
+  | '.' space* nl | '.' space* eof 
+	{ Output.char '.'; Output.line_break(); 
+	  if not !formatted then true else body_bol lexbuf }      
+  | '.' space+ { Output.char '.'; Output.char ' '; 
+	  if not !formatted then false else body lexbuf }
   | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
   | "(*" { comment_level := 1; 
+	   if !Cdglobals.parse_comments then Output.start_comment ();
 	   let eol = comment lexbuf in 
 	     if eol 
-	     then begin Output.line_break(); body_bol lexbuf end
+	     then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
 	     else body lexbuf }
   | identifier 
       { let s = lexeme lexbuf in 
@@ -680,7 +730,7 @@ and body = parse
 	  body lexbuf }
   | token_no_brackets
       { let s = lexeme lexbuf in
-	  Output.symbol s; body lexbuf }
+	  symbol lexbuf s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
 	  Output.char c; 
           body lexbuf }
@@ -695,7 +745,7 @@ and notation = parse
   | '"' { Output.char '"'}
   | token
       { let s = lexeme lexbuf in
-	  Output.symbol s; notation lexbuf }
+	  symbol lexbuf s; notation lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
 	  Output.char c; 
           notation lexbuf }
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 04945040..1a1640a4 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -264,6 +264,14 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
+let push_named_context = List.fold_right push_named
+
+let rec list_filter_map f = function
+  | [] -> []
+  | hd :: tl -> match f hd with
+    | None -> list_filter_map f tl
+    | Some x -> x :: list_filter_map f tl
+
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let evars = ref (Evd.create_evar_defs Evd.empty) in
@@ -273,6 +281,14 @@ let context ?(hook=fun _ -> ()) l =
   List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
   let ctx = try named_of_rel_context fullctx with _ -> 
     error "Anonymous variables not allowed in contexts."
+  in
+  let env = push_named_context ctx env in
+  let keeps = 
+    List.fold_left (fun acc (id,_,t) ->
+      match class_of_constr t with
+      | None -> acc
+      | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc)
+      [] ctx
   in
     List.iter (function (id,_,t) -> 
       if Lib.is_modtype () then 
@@ -285,10 +301,14 @@ let context ?(hook=fun _ -> ()) l =
 		hook (ConstRef cst)
 	    | None -> ()
       else (
-	let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+	let impl = List.exists (fun (x,_) -> 
+	  match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls 
+	and keep = 
+	  let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in
+	    List.concat l
 	in
 	  Command.declare_one_assumption false (Local (* global *), Definitional) t
-	    [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
+	    [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id);
 	  match class_of_constr t with
 	  | None -> ()
 	  | Some tc -> hook (VarRef id)))
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b50c9bbd..05a22829 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: command.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -546,7 +546,7 @@ let interp_mutual paramsl indl notations finite =
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
-    States.with_heavy_rollback (fun () -> 
+    States.with_state_protection (fun () -> 
      (* Temporary declaration of notations and scopes *)
      List.iter (declare_interning_data impls) notations;
      (* Interpret the constructor types *)
@@ -851,7 +851,7 @@ let interp_recursive fixkind l boxed =
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs = 
-    States.with_heavy_rollback (fun () -> 
+    States.with_state_protection (fun () -> 
       List.iter (declare_interning_data impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
@@ -1012,16 +1012,18 @@ let build_combined_scheme name schemes =
     let (ctx, arity) = decompose_prod ty in
     let (_, last) = List.hd ctx in
       match kind_of_term last with
-	| App (ind, args) -> ctx, destInd ind, Array.length args
+	| App (ind, args) -> 
+	    let ind = destInd ind in
+	    let (_,spec) = Inductive.lookup_mind_specif env ind in
+	      ctx, ind, spec.mind_nrealargs
 	| _ -> ctx, destInd last, 0
   in
   let defs =  
     List.map (fun x -> 
 		let refe = Ident x in
 		let qualid = qualid_of_reference refe in
-		let cst = try 
-                    Nametab.locate_constant (snd qualid) 
-                with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
+		let cst = try Nametab.locate_constant (snd qualid) 
+                  with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
                 in
 		let ty = Typeops.type_of_constant env cst in
 		  qualid, cst, ty)
@@ -1087,9 +1089,9 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
   | None ->
       (match local with
       | Local ->
-          let impl=false and keep=false in (* copy values from Vernacentries *)
+          let impl=false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum (t_i,impl,keep) in
+          let c = SectionLocalAssum (t_i,impl,[]) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
           (Local,VarRef id,imps)
       | Global ->
@@ -1123,9 +1125,9 @@ let look_for_mutual_statements thms =
     let n = List.length thms in
     let inds = List.map (fun (id,(t,_) as x) -> 
       let (hyps,ccl) = Sign.decompose_prod_assum t in
-      let whnf_hyp_hds = map_rel_context_with_binders
-        (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c)))
-        hyps in
+      let whnf_hyp_hds = fold_map_rel_context
+        (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
+	(Global.env()) hyps in
       let ind_hyps =
         List.flatten (list_map_i (fun i (_,b,t) ->
           match kind_of_term t with
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b42fafd0..36399029 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: command.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
+(*i $Id: command.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -45,13 +45,13 @@ val syntax_definition : identifier -> identifier list * constr_expr ->
 
 val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
   Impargs.manual_explicitation list ->
-  bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
+  bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
   
 val set_declare_assumption_hook : (types -> unit) -> unit
 
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> 
-  bool -> bool -> bool -> unit
+  bool -> identifier list -> bool -> unit
 
 val declare_interning_data : 'a * Constrintern.implicits_env ->
     string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f733a3d5..0cda7c71 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: himsg.ml 11986 2009-03-17 11:44:20Z herbelin $ *)
 
 open Pp
 open Util
@@ -814,8 +814,8 @@ let explain_ltac_call_trace (last,trace,loc) =
       (if unboundvars <> [] or vars <> [] then
 	strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) -> 
 	pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
-	  (List.rev vars @ unboundvars)
-       else mt()) ++ str ")" in
+	  (List.rev vars @ unboundvars) ++ str ")"
+       else mt()) in
   if calls <> [] then
     let kind_of_last_call = match list_last calls with
     | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 4a2ef7db..4c0e34cd 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: record.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id: record.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
 
 open Pp
 open Util
@@ -366,7 +366,7 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   (* Now, younger decl in params and fields is on top *)
   let sc = Option.map mkSort s in
   let implpars, params, implfs, fields = 
-    States.with_heavy_rollback (fun () ->
+    States.with_state_protection (fun () ->
       typecheck_params_and_fields idstruc sc ps notations fs) ()
   in
     match kind with
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c95c89d3..6a0acb52 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
+(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -373,7 +373,7 @@ let vernac_assumption kind l nl=
 	List.iter (fun lid -> 
 	  if global then Dumpglob.dump_definition lid false "ax" 
 	  else Dumpglob.dump_definition lid true "var") idl;
-      declare_assumption idl is_coe kind [] c false false nl) l
+      declare_assumption idl is_coe kind [] c false [] nl) l
 
 let vernac_record k finite struc binders sort nameopt cfs =
   let const = match nameopt with 
@@ -807,14 +807,6 @@ let _ =
       optread  = Impargs.is_implicit_args;
       optwrite = Impargs.make_implicit_args }
 
-let _ =
-  declare_bool_option 
-    { optsync  = true;
-      optname  = "manual implicit arguments";
-      optkey   = (TertiaryTable ("Manual","Implicit","Arguments"));
-      optread  = Impargs.is_manual_implicit_args;
-      optwrite = Impargs.make_manual_implicit_args }
-
 let _ =
   declare_bool_option 
     { optsync  = true;
@@ -1110,9 +1102,10 @@ let vernac_print = function
   | PrintAbout qid -> msgnl (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
 (*spiwack: prints all the axioms and section variables used by a term *)
-  | PrintAssumptions r ->
+  | PrintAssumptions (o,r) ->
       let cstr = constr_of_global (global_with_alias r) in
-      let nassumptions = Environ.assumptions cstr (Global.env ()) in
+      let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ())
+	~add_opaque:o cstr (Global.env ()) in
       msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
 
 let global_module r =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3e9dfb25..4da16ea7 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacexpr.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
+(*i $Id: vernacexpr.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 open Util
 open Names
@@ -65,7 +65,7 @@ type printable =
   | PrintVisibility of string option
   | PrintAbout of reference
   | PrintImplicit of reference
-  | PrintAssumptions of reference
+  | PrintAssumptions of bool * reference
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
-- 
cgit v1.2.3