122 files changed, 284 insertions, 302 deletions

diff --git a/.merlin b/.merlin
index 21555f5e5d..d60f5037bb 100644
--- a/.merlin
+++ b/.merlin
@@ -1,17 +1,17 @@
 FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50
 
+S clib
+B clib
 S config
 B config
-S ide
-B ide
 S lib
 B lib
-S intf
-B intf
 S kernel
 B kernel
 S kernel/byterun
 B kernel/byterun
+S intf
+B intf
 S library
 B library
 S engine
@@ -30,14 +30,16 @@ S parsing
 B parsing
 S stm
 B stm
-S toplevel
-B toplevel
 S vernac
 B vernac
+S toplevel
+B toplevel
 S plugins/ltac
 B plugins/ltac
 S API
 B API
+S ide
+B ide
 
 S tools
 B tools
diff --git a/API/API.mli b/API/API.mli
index 24a99d57f6..def60ec267 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1443,9 +1443,9 @@ sig
   type record_body = (Id.t * Constant.t array * projection_body array) option
 
   type recursivity_kind =
-    | Finite
-    | CoFinite
-    | BiFinite
+    | Finite (** = inductive *)
+    | CoFinite (** = coinductive *)
+    | BiFinite (** = non-recursive, like in "Record" definitions *)
 
   type mutual_inductive_body = {
         mind_packets : one_inductive_body array;
@@ -2160,10 +2160,14 @@ module Decl_kinds :
 sig
   type polymorphic = bool
   type cumulative_inductive_flag = bool
+
   type recursivity_kind = Declarations.recursivity_kind =
-    | Finite
-    | CoFinite
-    | BiFinite
+    | Finite (** = inductive *)
+        [@ocaml.deprecated "Please use [Declarations.Finite"]
+    | CoFinite (** = coinductive *)
+        [@ocaml.deprecated "Please use [Declarations.CoFinite"]
+    | BiFinite (** = non-recursive, like in "Record" definitions *)
+        [@ocaml.deprecated "Please use [Declarations.BiFinite"]
   [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
 
   type discharge =
@@ -4308,7 +4312,7 @@ sig
   type typeclass = {
     cl_univs : Univ.AUContext.t;
     cl_impl : Globnames.global_reference;
-    cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t;
+    cl_context : Globnames.global_reference option list * Context.Rel.t;
     cl_props : Context.Rel.t;
     cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option
                 * Names.Constant.t option) list;
diff --git a/META.coq b/META.coq
index d31b60cd02..75cec8f0cf 100644
--- a/META.coq
+++ b/META.coq
@@ -23,19 +23,27 @@ package "config" (
 
 )
 
+package "clib" (
+  description = "Base General Coq Library"
+  version     = "8.7"
+
+  directory   = "clib"
+  requires    = "str, unix, threads"
+
+  archive(byte)    = "clib.cma"
+  archive(native)  = "clib.cmxa"
+)
+
 package "lib" (
 
-  description = "Base Coq Library"
+  description = "Base Coq-Specific Library"
   version     = "8.7"
 
   directory   = "lib"
 
-  requires         = "str, unix, threads, coq.config"
+  requires    = "coq.clib, coq.config"
 
-  archive(byte)    = "clib.cma"
   archive(byte)   += "lib.cma"
-
-  archive(native)  = "clib.cmxa"
   archive(native) += "lib.cmxa"
 
 )
diff --git a/Makefile.build b/Makefile.build
index 2f7ce6ef35..33ab72e689 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -195,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 COQOPTS=$(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
 
-LOCALINCLUDES=$(if $(filter plugins/%,$@),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS)))
+LOCALINCLUDES=$(if $(filter plugins/%,$@),-I clib -I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS)))
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
 OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
@@ -417,7 +417,7 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP)
 
 # coqc
 
-COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo
+COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
 
 $(COQC): $(call bestobj, $(COQCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -438,21 +438,21 @@ tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT)
 # Remember to update the dependencies below when you add files!
 
 COQDEPBOOTSRC := \
- lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \
+ clib/segmenttree.cmo clib/unicodetable.cmo clib/unicode.cmo clib/minisys.cmo \
  tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo
 
-lib/segmenttree.cmo : lib/segmenttree.cmi
-lib/segmenttree.cmx : lib/segmenttree.cmi
-lib/unicodetable.cmo : lib/segmenttree.cmo
-lib/unicodetable.cmx : lib/segmenttree.cmx
-lib/unicode.cmo : lib/unicodetable.cmo lib/unicode.cmi
-lib/unicode.cmx : lib/unicodetable.cmx lib/unicode.cmi
-lib/minisys.cmo : lib/unicode.cmo
-lib/minisys.cmx : lib/unicode.cmx
-tools/coqdep_lexer.cmo : lib/unicode.cmi tools/coqdep_lexer.cmi
-tools/coqdep_lexer.cmx : lib/unicode.cmx tools/coqdep_lexer.cmi
-tools/coqdep_common.cmo : lib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi
-tools/coqdep_common.cmx : lib/minisys.cmx tools/coqdep_lexer.cmx tools/coqdep_common.cmi
+clib/segmenttree.cmo : clib/segmenttree.cmi
+clib/segmenttree.cmx : clib/segmenttree.cmi
+clib/unicodetable.cmo : clib/segmenttree.cmo
+clib/unicodetable.cmx : clib/segmenttree.cmx
+clib/unicode.cmo : clib/unicodetable.cmo clib/unicode.cmi
+clib/unicode.cmx : clib/unicodetable.cmx clib/unicode.cmi
+clib/minisys.cmo : clib/unicode.cmo
+clib/minisys.cmx : clib/unicode.cmx
+tools/coqdep_lexer.cmo : clib/unicode.cmi tools/coqdep_lexer.cmi
+tools/coqdep_lexer.cmx : clib/unicode.cmx tools/coqdep_lexer.cmi
+tools/coqdep_common.cmo : clib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi
+tools/coqdep_common.cmx : clib/minisys.cmx tools/coqdep_lexer.cmx tools/coqdep_common.cmi
 tools/coqdep_boot.cmo : tools/coqdep_common.cmi
 tools/coqdep_boot.cmx : tools/coqdep_common.cmx
 
@@ -466,10 +466,8 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
 
 # The full coqdep (unused by this build, but distributed by make install)
 
-COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \
-  lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \
-  lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \
-  tools/coqdep.cmo
+COQDEPCMO:=clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo	\
+  tools/coqdep_common.cmo tools/coqdep.cmo
 
 $(COQDEP): $(call bestobj, $(COQDEPCMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -479,7 +477,7 @@ $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,)
 
-COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo
+COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo
 
 $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -493,23 +491,24 @@ $(COQWC): $(call bestobj, tools/coqwc.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package str)
 
-COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \
+COQDOCCMO:=clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
 
 $(COQDOC): $(call bestobj, $(COQDOCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package str,unix)
 
-$(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
+$(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, $(SYSMOD))
 
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo	ide/document.cmo \
- ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \
- ide/richpp.cmo ide/xmlprotocol.cmo tools/fake_ide.cmo
+FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo	\
+ ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo	\
+ ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo	\
+ tools/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -517,7 +516,7 @@ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 
 # votour: a small vo explorer (based on the checker)
 
-bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo)
+bin/votour: $(call bestobj, clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I checker)
 
@@ -525,7 +524,7 @@ bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo
 # Csdp to micromega special targets
 ###########################################################################
 
-CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \
+CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \
   mutils.cmo 	micromega.cmo \
   sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
 
@@ -581,7 +580,7 @@ kernel/kernel.cma: kernel/kernel.mllib
 # Make sure that API/API.mli cannot leak types from the Coq codebase.
 API/API.cmi : API/API.mli
 	$(SHOW)'OCAMLC    $<'
-	$(HIDE)$(OCAMLC) -I lib -I $(MYCAMLP4LIB) -c $<
+	$(HIDE)$(OCAMLC) -I clib -I lib -I $(MYCAMLP4LIB) -c $<
 
 %.cma: %.mllib
 	$(SHOW)'OCAMLC -a -o $@'
diff --git a/Makefile.checker b/Makefile.checker
index 7e0f588759..5b5855782f 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -20,7 +20,7 @@ CHICKEN:=bin/coqchk$(EXE)
 
 # The sources
 
-CHKLIBS:= -I config -I lib -I checker
+CHKLIBS:= -I config -I clib -I lib -I checker
 
 ## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread
 
diff --git a/Makefile.common b/Makefile.common
index f436d3e8f1..7e8f3e3e74 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -73,7 +73,7 @@ INSTALLSH:=./install.sh
 MKDIR:=install -d
 
 CORESRCDIRS:=\
-  config 	lib		kernel	intf	kernel/byterun	library \
+  config 	clib 		lib		kernel	intf	kernel/byterun	library \
   engine 	pretyping	interp	proofs	parsing 	printing \
   tactics 	vernac		stm		toplevel 	API
 
@@ -100,7 +100,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
-CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
+CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
 	stm/stm.cma toplevel/toplevel.cma API/API.cma
diff --git a/Makefile.ide b/Makefile.ide
index 7d809f67a5..08829b5544 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -41,7 +41,7 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
 
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
-IDEDEPS:=lib/clib.cma lib/cErrors.cmo lib/spawn.cmo
+IDEDEPS:=clib/clib.cma lib/lib.cma
 IDECMA:=ide/ide.cma
 IDETOPLOOPCMA=ide/coqidetop.cma
 
diff --git a/lib/backtrace.ml b/clib/backtrace.ml
index be9f40c1fb..be9f40c1fb 100644
--- a/lib/backtrace.ml
+++ b/clib/backtrace.ml
diff --git a/lib/backtrace.mli b/clib/backtrace.mli
index dd82165b6d..dd82165b6d 100644
--- a/lib/backtrace.mli
+++ b/clib/backtrace.mli
diff --git a/lib/bigint.ml b/clib/bigint.ml
index 4f8b95d592..4f8b95d592 100644
--- a/lib/bigint.ml
+++ b/clib/bigint.ml
diff --git a/lib/bigint.mli b/clib/bigint.mli
index 2a5a5f122d..2a5a5f122d 100644
--- a/lib/bigint.mli
+++ b/clib/bigint.mli
diff --git a/lib/cArray.ml b/clib/cArray.ml
index 013585735c..013585735c 100644
--- a/lib/cArray.ml
+++ b/clib/cArray.ml
diff --git a/lib/cArray.mli b/clib/cArray.mli
index 325ff8edcc..325ff8edcc 100644
--- a/lib/cArray.mli
+++ b/clib/cArray.mli
diff --git a/lib/cEphemeron.ml b/clib/cEphemeron.ml
index 8b253a7901..8b253a7901 100644
--- a/lib/cEphemeron.ml
+++ b/clib/cEphemeron.ml
diff --git a/lib/cEphemeron.mli b/clib/cEphemeron.mli
index d8a1f27573..d8a1f27573 100644
--- a/lib/cEphemeron.mli
+++ b/clib/cEphemeron.mli
diff --git a/lib/cList.ml b/clib/cList.ml
index 0ef7c3d8ba..0ef7c3d8ba 100644
--- a/lib/cList.ml
+++ b/clib/cList.ml
diff --git a/lib/cList.mli b/clib/cList.mli
index f87db04cf4..f87db04cf4 100644
--- a/lib/cList.mli
+++ b/clib/cList.mli
diff --git a/lib/cMap.ml b/clib/cMap.ml
index b4c4aedd0e..b4c4aedd0e 100644
--- a/lib/cMap.ml
+++ b/clib/cMap.ml
diff --git a/lib/cMap.mli b/clib/cMap.mli
index 5e65bd200a..5e65bd200a 100644
--- a/lib/cMap.mli
+++ b/clib/cMap.mli
diff --git a/lib/cObj.ml b/clib/cObj.ml
index 7f3ee18553..7f3ee18553 100644
--- a/lib/cObj.ml
+++ b/clib/cObj.ml
diff --git a/lib/cObj.mli b/clib/cObj.mli
index 16933a4aa4..16933a4aa4 100644
--- a/lib/cObj.mli
+++ b/clib/cObj.mli
diff --git a/lib/cSet.ml b/clib/cSet.ml
index ed65edf16e..ed65edf16e 100644
--- a/lib/cSet.ml
+++ b/clib/cSet.ml
diff --git a/lib/cSet.mli b/clib/cSet.mli
index 2eb9bce869..2eb9bce869 100644
--- a/lib/cSet.mli
+++ b/clib/cSet.mli
diff --git a/lib/cSig.mli b/clib/cSig.mli
index 32e9d2af0c..32e9d2af0c 100644
--- a/lib/cSig.mli
+++ b/clib/cSig.mli
diff --git a/lib/cStack.ml b/clib/cStack.ml
index 4acb2930c5..4acb2930c5 100644
--- a/lib/cStack.ml
+++ b/clib/cStack.ml
diff --git a/lib/cStack.mli b/clib/cStack.mli
index 8dde1d1a1a..8dde1d1a1a 100644
--- a/lib/cStack.mli
+++ b/clib/cStack.mli
diff --git a/lib/cString.ml b/clib/cString.ml
index f2242460e8..f2242460e8 100644
--- a/lib/cString.ml
+++ b/clib/cString.ml
diff --git a/lib/cString.mli b/clib/cString.mli
index 29d3a44995..29d3a44995 100644
--- a/lib/cString.mli
+++ b/clib/cString.mli
diff --git a/lib/cThread.ml b/clib/cThread.ml
index 0221e690e8..0221e690e8 100644
--- a/lib/cThread.ml
+++ b/clib/cThread.ml
diff --git a/lib/cThread.mli b/clib/cThread.mli
index 66f039bb52..66f039bb52 100644
--- a/lib/cThread.mli
+++ b/clib/cThread.mli
diff --git a/lib/cUnix.ml b/clib/cUnix.ml
index 34fb660db4..34fb660db4 100644
--- a/lib/cUnix.ml
+++ b/clib/cUnix.ml
diff --git a/lib/cUnix.mli b/clib/cUnix.mli
index d08dc4c403..d08dc4c403 100644
--- a/lib/cUnix.mli
+++ b/clib/cUnix.mli
diff --git a/lib/canary.ml b/clib/canary.ml
index 0ed1d28f37..0ed1d28f37 100644
--- a/lib/canary.ml
+++ b/clib/canary.ml
diff --git a/lib/canary.mli b/clib/canary.mli
index 904b88213c..904b88213c 100644
--- a/lib/canary.mli
+++ b/clib/canary.mli
diff --git a/lib/clib.mllib b/clib/clib.mllib
index 5c1f7d9af8..bd5ddb1525 100644
--- a/lib/clib.mllib
+++ b/clib/clib.mllib
@@ -1,37 +1,38 @@
-Coq_config
-
-Terminal
 Canary
-Hook
+CObj
+CEphemeron
+
 Hashset
 Hashcons
+
 CSet
 CMap
+CList
+CString
+CStack
+
 Int
-Dyn
 HMap
+Bigint
+
+CArray
 Option
+CUnix
+
+Segmenttree
+Unicodetable
+Unicode
+Minisys
+CThread
+Trie
+Predicate
+Heap
+Unionfind
+
+Dyn
 Store
 Exninfo
 Backtrace
 IStream
-Flags
-Control
-Loc
-CAst
-DAst
-CList
-CString
-Deque
-CObj
-CArray
-CStack
-Util
-Stateid
-Pp
-Feedback
-CUnix
-Envars
-Aux_file
+Terminal
 Monad
-CoqProject_file
diff --git a/lib/deque.ml b/clib/deque.ml
index 373269b4f5..373269b4f5 100644
--- a/lib/deque.ml
+++ b/clib/deque.ml
diff --git a/lib/deque.mli b/clib/deque.mli
index 23cb1e4919..23cb1e4919 100644
--- a/lib/deque.mli
+++ b/clib/deque.mli
diff --git a/lib/dyn.ml b/clib/dyn.ml
index 64535d35f6..64535d35f6 100644
--- a/lib/dyn.ml
+++ b/clib/dyn.ml
diff --git a/lib/dyn.mli b/clib/dyn.mli
index 2206394e2d..2206394e2d 100644
--- a/lib/dyn.mli
+++ b/clib/dyn.mli
diff --git a/lib/exninfo.ml b/clib/exninfo.ml
index 167d3d6dc8..167d3d6dc8 100644
--- a/lib/exninfo.ml
+++ b/clib/exninfo.ml
diff --git a/lib/exninfo.mli b/clib/exninfo.mli
index c960ac7c08..c960ac7c08 100644
--- a/lib/exninfo.mli
+++ b/clib/exninfo.mli
diff --git a/lib/hMap.ml b/clib/hMap.ml
index 37079af783..37079af783 100644
--- a/lib/hMap.ml
+++ b/clib/hMap.ml
diff --git a/lib/hMap.mli b/clib/hMap.mli
index c77bfced88..c77bfced88 100644
--- a/lib/hMap.mli
+++ b/clib/hMap.mli
diff --git a/lib/hashcons.ml b/clib/hashcons.ml
index ee22325811..ee22325811 100644
--- a/lib/hashcons.ml
+++ b/clib/hashcons.ml
diff --git a/lib/hashcons.mli b/clib/hashcons.mli
index fbd2ebcf9a..fbd2ebcf9a 100644
--- a/lib/hashcons.mli
+++ b/clib/hashcons.mli
diff --git a/lib/hashset.ml b/clib/hashset.ml
index 7f96627a68..7f96627a68 100644
--- a/lib/hashset.ml
+++ b/clib/hashset.ml
diff --git a/lib/hashset.mli b/clib/hashset.mli
index ec79205a5c..ec79205a5c 100644
--- a/lib/hashset.mli
+++ b/clib/hashset.mli
diff --git a/lib/heap.ml b/clib/heap.ml
index a6109972d7..a6109972d7 100644
--- a/lib/heap.ml
+++ b/clib/heap.ml
diff --git a/lib/heap.mli b/clib/heap.mli
index 93d504c5ac..93d504c5ac 100644
--- a/lib/heap.mli
+++ b/clib/heap.mli
diff --git a/lib/iStream.ml b/clib/iStream.ml
index d3a54332a1..d3a54332a1 100644
--- a/lib/iStream.ml
+++ b/clib/iStream.ml
diff --git a/lib/iStream.mli b/clib/iStream.mli
index cd7940e8d3..cd7940e8d3 100644
--- a/lib/iStream.mli
+++ b/clib/iStream.mli
diff --git a/lib/int.ml b/clib/int.ml
index 63f62154d8..63f62154d8 100644
--- a/lib/int.ml
+++ b/clib/int.ml
diff --git a/lib/int.mli b/clib/int.mli
index b65367f7d4..b65367f7d4 100644
--- a/lib/int.mli
+++ b/clib/int.mli
diff --git a/lib/minisys.ml b/clib/minisys.ml
index 389b18ad4e..389b18ad4e 100644
--- a/lib/minisys.ml
+++ b/clib/minisys.ml
diff --git a/lib/monad.ml b/clib/monad.ml
index 2e55e9698c..2e55e9698c 100644
--- a/lib/monad.ml
+++ b/clib/monad.ml
diff --git a/lib/monad.mli b/clib/monad.mli
index 7b0a3e600f..7b0a3e600f 100644
--- a/lib/monad.mli
+++ b/clib/monad.mli
diff --git a/lib/option.ml b/clib/option.ml
index 98b1680354..98b1680354 100644
--- a/lib/option.ml
+++ b/clib/option.ml
diff --git a/lib/option.mli b/clib/option.mli
index 66f05023f7..66f05023f7 100644
--- a/lib/option.mli
+++ b/clib/option.mli
diff --git a/lib/predicate.ml b/clib/predicate.ml
index 1aa7db6af1..1aa7db6af1 100644
--- a/lib/predicate.ml
+++ b/clib/predicate.ml
diff --git a/lib/predicate.mli b/clib/predicate.mli
index cee3b0bd39..cee3b0bd39 100644
--- a/lib/predicate.mli
+++ b/clib/predicate.mli
diff --git a/lib/segmenttree.ml b/clib/segmenttree.ml
index d0ded4cb59..d0ded4cb59 100644
--- a/lib/segmenttree.ml
+++ b/clib/segmenttree.ml
diff --git a/lib/segmenttree.mli b/clib/segmenttree.mli
index e274a6fdc8..e274a6fdc8 100644
--- a/lib/segmenttree.mli
+++ b/clib/segmenttree.mli
diff --git a/lib/store.ml b/clib/store.ml
index 97a8fea085..97a8fea085 100644
--- a/lib/store.ml
+++ b/clib/store.ml
diff --git a/lib/store.mli b/clib/store.mli
index 5cc5bb8593..5cc5bb8593 100644
--- a/lib/store.mli
+++ b/clib/store.mli
diff --git a/lib/terminal.ml b/clib/terminal.ml
index 34efddfbca..34efddfbca 100644
--- a/lib/terminal.ml
+++ b/clib/terminal.ml
diff --git a/lib/terminal.mli b/clib/terminal.mli
index b1b76e6e2a..b1b76e6e2a 100644
--- a/lib/terminal.mli
+++ b/clib/terminal.mli
diff --git a/lib/trie.ml b/clib/trie.ml
index 0b0ba27613..0b0ba27613 100644
--- a/lib/trie.ml
+++ b/clib/trie.ml
diff --git a/lib/trie.mli b/clib/trie.mli
index a87acc8a69..a87acc8a69 100644
--- a/lib/trie.mli
+++ b/clib/trie.mli
diff --git a/lib/unicode.ml b/clib/unicode.ml
index f193c4e0f8..f193c4e0f8 100644
--- a/lib/unicode.ml
+++ b/clib/unicode.ml
diff --git a/lib/unicode.mli b/clib/unicode.mli
index 32ffbb8e94..32ffbb8e94 100644
--- a/lib/unicode.mli
+++ b/clib/unicode.mli
diff --git a/lib/unicodetable.ml b/clib/unicodetable.ml
index b607058c64..b607058c64 100644
--- a/lib/unicodetable.ml
+++ b/clib/unicodetable.ml
diff --git a/lib/unionfind.ml b/clib/unionfind.ml
index f9c92d6a8e..f9c92d6a8e 100644
--- a/lib/unionfind.ml
+++ b/clib/unionfind.ml
diff --git a/lib/unionfind.mli b/clib/unionfind.mli
index b242232edb..b242232edb 100644
--- a/lib/unionfind.mli
+++ b/clib/unionfind.mli
diff --git a/configure.ml b/configure.ml
index 06aa5e7666..0698d93e26 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1143,7 +1143,7 @@ let write_configml f =
                                     core_src_dirs in
 
   pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs;
-  pr "\nlet api_dirs = [\"API\"; \"lib\"]\n";
+  pr "\nlet api_dirs = [\"API\"; \"clib\"; \"lib\"]\n";
   pr "\nlet plugins_dirs = [\n";
 
   let plugins = Sys.readdir "plugins" in
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 23131c94c6..58c90ff11d 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -5,8 +5,17 @@ set -xe
 if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN=`pwd`/_install_ci/bin
-    export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME"
+    export CI_BRANCH="$CI_COMMIT_REF_NAME"
 else
+    if [ -n "${TRAVIS}" ];
+    then
+        export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
+        export CI_BRANCH="$TRAVIS_BRANCH"
+    elif [ -n "${CIRCLECI}" ];
+    then
+        export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
+        export CI_BRANCH="$CIRCLE_BRANCH"
+    fi
     export COQBIN=`pwd`/bin
 fi
 export PATH="$COQBIN:$PATH"
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
index af4a96f4ae..7716bcb59a 100644
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -1,4 +1,4 @@
-if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
diff --git a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh
deleted file mode 100644
index 5c4dd1324f..0000000000
--- a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then
-    formal_topology_CI_BRANCH=ci
-    formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git
-
-    HoTT_CI_BRANCH=coq-pr-1033
-    HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git
-
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
deleted file mode 100644
index cdca8e525a..0000000000
--- a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then
-    ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer
-    ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git
-fi
diff --git a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh
deleted file mode 100644
index 6741cf26fb..0000000000
--- a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6169" ] || [ "$TRAVIS_BRANCH" = "clean-up/deprecated-options" ]; then
-    ltac2_CI_BRANCH=master
-    ltac2_CI_GITURL=https://github.com/Zimmi48/ltac2
-fi
diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
deleted file mode 100644
index c9f1272bed..0000000000
--- a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then
-    ltac2_CI_BRANCH=localityfixyou
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git
-fi
diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh
deleted file mode 100644
index 68e1901f7f..0000000000
--- a/dev/ci/user-overlays/06217-coqdep-at-once.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6217" ] || [ "$TRAVIS_BRANCH" = "coqdep-at-once" ]; then
-    UniMath_CI_GITURL=https://github.com/SkySkimmer/UniMath.git
-fi
diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh
deleted file mode 100644
index 7e9b5febdd..0000000000
--- a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then
-    Equations_CI_BRANCH=fix-coq-6324
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh
deleted file mode 100644
index c0dcf79e1d..0000000000
--- a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6392" ] || [ "$TRAVIS_BRANCH" = "econstr+fix_class" ]; then
-    Equations_CI_BRANCH=econstr+fix_class
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
deleted file mode 100644
index 8aea7dee3a..0000000000
--- a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then
-    Equations_CI_BRANCH=interp+less_impstyle_p2
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 9146d3d521..9f0377ceea 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
 ```
-if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
 ```
+
+(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh))
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 0b33dab051..c52a0040bf 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -45,7 +45,7 @@ let rec make_let raw e = function
       <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let raw e l
 
-let make_clause (pt,_,e) =
+let make_clause (pt,e) =
   (make_patt pt,
    ploc_vala None,
    make_let false e pt)
@@ -76,7 +76,7 @@ let make_prod_item = function
     <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option mlexpr_of_ident id$ ) ) >>
 
 let mlexpr_of_clause cl =
-  mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
+  mlexpr_of_list (fun (a,_) -> mlexpr_of_list make_prod_item a) cl
 
 (** Special treatment of constr entries *)
 let is_constr_gram = function
@@ -88,8 +88,8 @@ let make_var = function
   | ExtNonTerminal (_, p) -> p
   | _ -> assert false
 
-let declare_tactic loc tacname ~level classification clause = match clause with
-| [(ExtTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
+let declare_tactic loc tacname ~level clause = match clause with
+| [(ExtTerminal name) :: rem, tac] when List.for_all is_constr_gram rem ->
   (** The extension is only made of a name followed by constr entries: we do not
       add any grammar nor printing rule and add it as a true Ltac definition. *)
   let patt = make_patt rem in
@@ -141,16 +141,14 @@ EXTEND
   str_item:
     [ [ "TACTIC"; "EXTEND"; s = tac_name;
         level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
-        c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
         let level = match level with Some i -> int_of_string i | None -> 0 in
-         declare_tactic loc s ~level c l ] ]
+         declare_tactic loc s ~level l ] ]
   ;
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
-        c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ];
-        "->"; "["; e = Pcaml.expr; "]" -> (l,c,e)
+        "->"; "["; e = Pcaml.expr; "]" -> (l,e)
     ] ]
   ;
   tacargs:
diff --git a/interp/declare.ml b/interp/declare.ml
index 5be07e09ec..d1b79ffcdd 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -349,7 +349,7 @@ let dummy_one_inductive_entry mie = {
 let dummy_inductive_entry (_,m) = ([],{
   mind_entry_params = [];
   mind_entry_record = None;
-  mind_entry_finite = Decl_kinds.BiFinite;
+  mind_entry_finite = Declarations.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
   mind_entry_private = None;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 0197cf9ae2..d7962e29a6 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -68,6 +68,7 @@ let pause () = previous_state := !glob_output; glob_output := NoGlob
 let continue () = glob_output := !previous_state
 
 open Decl_kinds
+open Declarations
 
 let type_of_logical_kind = function
   | IsDefinition def ->
@@ -111,14 +112,12 @@ let type_of_global_ref gr =
     | Globnames.IndRef ind ->
 	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
 	  if mib.Declarations.mind_record <> None then
-            let open Decl_kinds in
             begin match mib.Declarations.mind_finite with
             | Finite -> "indrec"
             | BiFinite -> "rec"
 	    | CoFinite -> "corec"
             end
 	  else
-            let open Decl_kinds in
             begin match mib.Declarations.mind_finite with
             | Finite -> "ind"
             | BiFinite -> "variant"
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index f7c36c4e5f..bfe73160bb 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
+  Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
   Constrexpr.constr_expr * Id.Set.t
 
 val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
+  (Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
     Constrexpr.constr_expr * Id.Set.t) ->
   constr_expr -> constr_expr * Id.Set.t
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index b0c1f66613..b9a3f0c212 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -77,6 +77,9 @@ type logical_kind =
 
 type recursivity_kind = Declarations.recursivity_kind =
   | Finite (** = inductive *)
+      [@ocaml.deprecated "Please use [Declarations.Finite"]
   | CoFinite (** = coinductive *)
+      [@ocaml.deprecated "Please use [Declarations.CoFinite"]
   | BiFinite (** = non-recursive, like in "Record" definitions *)
+      [@ocaml.deprecated "Please use [Declarations.BiFinite"]
 [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 31ded9129a..11616da7b3 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -810,7 +810,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (_,projs,pbs)) when
-	mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
+        mib.Declarations.mind_finite == Declarations.BiFinite ->
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8e9b606a58..1f2ae0b6cc 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -710,7 +710,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
     best-effort fashion. *)
 let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
   let ntypes = Array.length inds in
-  let recursive = finite != Decl_kinds.BiFinite in
+  let recursive = finite != BiFinite in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
   let ra_env_ar = Array.rev_to_list rc in
   let nparamsctxt = Context.Rel.length paramsctxt in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2a629f00a9..28a09b81b0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -38,14 +38,14 @@ let find_inductive env c =
   let (t, l) = decompose_app (whd_all env c) in
   match kind t with
     | Ind ind
-        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
+        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
   let (t, l) = decompose_app (whd_all env c) in
   match kind t with
     | Ind ind
-        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
+        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let inductive_params (mib,_) = mib.mind_nparams
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index de4dc21079..160a90dc2f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -515,7 +515,7 @@ let rec lambda_of_constr env sigma c =
 	    { asw_ind = ind;
           asw_ci = ci;
           asw_reloc = tbl; 
-          asw_finite = mib.mind_finite <> Decl_kinds.CoFinite;
+          asw_finite = mib.mind_finite <> CoFinite;
           asw_prefix = prefix}
       in
       (* translation of the argument *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2913c6dfad..d0d5cb1d56 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -193,7 +193,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       (arities_of_specif (mind, inst) (mib2, p2))
   in
   let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
-  check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
+  check (fun mib -> mib.mind_finite<>CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
   check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x);
   assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps);
   assert (Array.length mib1.mind_packets >= 1
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 970666638c..34f9aed37b 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -113,6 +113,7 @@ let exists_dir dir =
 
 
 let process_cmd_line orig_dir proj args =
+  let parsing_project_file = ref (proj.project_file <> None) in
   let orig_dir = (* avoids turning foo.v in ./foo.v *)
     if orig_dir = "." then "" else orig_dir in
   let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in
@@ -155,16 +156,22 @@ let process_cmd_line orig_dir proj args =
     aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r
 
   | "-f" :: file :: r ->
+    if !parsing_project_file then
+      raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file));
     let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
     let () = match proj.project_file with
       | None -> ()
       | Some _ -> Feedback.msg_warning (Pp.str
 	"Multiple project files are deprecated.")
     in
+    parsing_project_file := true;
     let proj = aux { proj with project_file = Some file } (parse file) in
+    parsing_project_file := false;
     aux proj r
 
   | "-o" :: file :: r ->
+    if !parsing_project_file then
+     raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file));
     if String.contains file '/' then
       error "Output file must be in the current directory";
     if proj.makefile <> None then
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 66f939a910..b2260ba097 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,21 +1,30 @@
+Coq_config
+
+Hook
+Flags
+Control
+Util
+
+Pp
+Stateid
+Loc
+Feedback
 CErrors
 CWarnings
-Bigint
-Segmenttree
-Unicodetable
-Unicode
-Minisys
+
+Rtree
 System
-CThread
-Spawn
-Trie
-CProfile
 Explore
-Predicate
-Rtree
-Heap
-Unionfind
-Genarg
-CEphemeron
+RTree
+CProfile
 Future
+Spawn
+
+CAst
+DAst
+Genarg
+
 RemoteCounter
+Aux_file
+Envars
+CoqProject_file
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c18c6810f7..29bcddaf41 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,6 +15,7 @@ open Constrexpr_ops
 open Extend
 open Vernacexpr
 open Decl_kinds
+open Declarations
 open Misctypes
 open Tok (* necessary for camlp4 *)
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 4ae875cd70..c169b7b50b 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -431,7 +431,7 @@ and extract_really_ind env kn mib =
 	let ip = (kn, 0) in
 	let r = IndRef ip in
 	if is_custom r then raise (I Standard);
-	if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive);
+        if mib.mind_finite == CoFinite then raise (I Coinductive);
 	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
 	let p,u = packets.(0) in
 	if p.ip_logical then raise (I Standard);
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 97066e5312..b4e17c5d1c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1498,7 +1498,7 @@ let do_build_inductive
   try
     with_full_print
       (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
-      Decl_kinds.Finite
+      Declarations.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
@@ -1509,7 +1509,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1524,7 +1524,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 9fcb35f89e..8f5d3f22f4 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -20,10 +20,10 @@ open Names
 open Term
 open Constr
 open Vars
-open Declarations
 open Glob_term
 open Glob_termops
 open Decl_kinds
+open Declarations
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -353,8 +353,8 @@ let ind2name = Id.of_string "__ind2"
     be co-inductive, and for the moment they must not be mutual
     either. *)
 let verify_inds mib1 mib2 =
-  if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive";
-  if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive";
+  if mib1.mind_finite == CoFinite then error "First argument is coinductive";
+  if mib2.mind_finite == CoFinite then error "Second argument is coinductive";
   if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual";
   if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual";
   ()
@@ -891,7 +891,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   (* Declare inductive *)
   let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in
   let mie,pl,impls = ComInductive.interp_mutual_inductive indl []
-          false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
+          false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Finite (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls)
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 9ae112d371..e5933de2a6 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -61,12 +61,9 @@ struct
 
 type t = Val.t
 
-let normalize v = v
-
 let of_constr c = in_gen (topwit wit_constr) c
 
 let to_constr v =
-  let v = normalize v in
   if has_type v (topwit wit_constr) then
     let c = out_gen (topwit wit_constr) v in
     Some c
@@ -78,7 +75,6 @@ let to_constr v =
 let of_uconstr c = in_gen (topwit wit_uconstr) c
 
 let to_uconstr v =
-  let v = normalize v in
   if has_type v (topwit wit_uconstr) then
     Some (out_gen (topwit wit_uconstr) v)
   else None
@@ -86,7 +82,6 @@ let to_uconstr v =
 let of_int i = in_gen (topwit wit_int) i
 
 let to_int v =
-  let v = normalize v in
   if has_type v (topwit wit_int) then
     Some (out_gen (topwit wit_int) v)
   else None
@@ -108,14 +103,12 @@ let constr_of_id env id =
 
 (* Gives the constr corresponding to a Constr_context tactic_arg *)
 let coerce_to_constr_context v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_constr_context) then
     out_gen (topwit wit_constr_context) v
   else raise (CannotCoerceTo "a term context")
 
 (* Interprets an identifier which must be fresh *)
 let coerce_var_to_ident fresh env sigma v =
-  let v = Value.normalize v in
   let fail () = raise (CannotCoerceTo "a fresh identifier") in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
@@ -140,7 +133,6 @@ let g = sigma in
 let id_of_name = function
   | Name.Anonymous -> Id.of_string "x"
   | Name.Name x -> x in
-  let v = Value.normalize v in
   let fail () = raise (CannotCoerceTo "an identifier") in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
@@ -179,7 +171,6 @@ let id_of_name = function
 
 
 let coerce_to_intro_pattern env sigma v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     snd (out_gen (topwit wit_intro_pattern) v)
   else if has_type v (topwit wit_var) then
@@ -198,7 +189,6 @@ let coerce_to_intro_pattern_naming env sigma v =
   | _ -> raise (CannotCoerceTo "a naming introduction pattern")
 
 let coerce_to_hint_base v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
     | _, IntroNaming (IntroIdentifier id) -> Id.to_string id
@@ -206,13 +196,11 @@ let coerce_to_hint_base v =
   else raise (CannotCoerceTo "a hint base name")
 
 let coerce_to_int v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_int) then
     out_gen (topwit wit_int) v
   else raise (CannotCoerceTo "an integer")
 
 let coerce_to_constr env v =
-  let v = Value.normalize v in
   let fail () = raise (CannotCoerceTo "a term") in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
@@ -230,7 +218,6 @@ let coerce_to_constr env v =
   else fail ()
 
 let coerce_to_uconstr env v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_uconstr) then
     out_gen (topwit wit_uconstr) v
   else
@@ -243,7 +230,6 @@ let coerce_to_closed_constr env v =
 
 let coerce_to_evaluable_ref env sigma v =
   let fail () = raise (CannotCoerceTo "an evaluable reference") in
-  let v = Value.normalize v in
   let ev =
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
@@ -284,7 +270,6 @@ let coerce_to_intro_pattern_list ?loc env sigma v =
 
 let coerce_to_hyp env sigma v =
   let fail () = raise (CannotCoerceTo "a variable") in
-  let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
     | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
@@ -306,7 +291,6 @@ let coerce_to_hyp_list env sigma v =
 
 (* Interprets a qualified name *)
 let coerce_to_reference env sigma v =
-  let v = Value.normalize v in
   match Value.to_constr v with
   | Some c ->
     begin
@@ -318,7 +302,6 @@ let coerce_to_reference env sigma v =
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
 let coerce_to_quantified_hypothesis sigma v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     let v = out_gen (topwit wit_intro_pattern) v in
     match v with
@@ -336,7 +319,6 @@ let coerce_to_quantified_hypothesis sigma v =
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
 let coerce_to_decl_or_quant_hyp env sigma v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index d7b253a687..dce16b7333 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -31,9 +31,6 @@ module Value :
 sig
   type t = Val.t
 
-  val normalize : t -> t
-  (** Eliminated the leading dynamic type casts. *)
-
   val of_constr : constr -> t
   val to_constr : t -> constr option
   val of_uconstr : Ltac_pretype.closed_glob_constr -> t
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ccded44179..f2720954d0 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -136,7 +136,6 @@ let to_tacvalue v = out_gen (topwit wit_tacvalue) v
 
 (** More naming applications *)
 let name_vfun appl vle =
-  let vle = Value.normalize vle in
   if has_type vle (topwit wit_tacvalue) then
     match to_tacvalue vle with
     | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t))
@@ -235,7 +234,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
 
 (* Displays a value *)
 let pr_value env v =
-  let v = Value.normalize v in
   let pr_with_env pr =
     match env with
     | Some (env,sigma) -> pr env sigma
@@ -285,7 +283,6 @@ let push_trace call ist = match TacStore.get ist.extra f_trace with
 | Some trace -> Proofview.tclUNIT (call :: trace)
 
 let propagate_trace ist loc id v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_tacvalue) then
     let tacv = to_tacvalue v in
     match tacv with
@@ -298,7 +295,6 @@ let propagate_trace ist loc id v =
   else Proofview.tclUNIT v
 
 let append_trace trace v =
-  let v = Value.normalize v in
   if has_type v (topwit wit_tacvalue) then
     match to_tacvalue v with
     | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b))
@@ -307,11 +303,9 @@ let append_trace trace v =
 
 (* Dynamically check that an argument is a tactic *)
 let coerce_to_tactic loc id v =
-  let v = Value.normalize v in
   let fail () = user_err ?loc 
     (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.")
   in
-  let v = Value.normalize v in
   if has_type v (topwit wit_tacvalue) then
     let tacv = to_tacvalue v in
     match tacv with
@@ -514,7 +508,6 @@ let rec intropattern_ids accu (loc,pat) = match pat with
 
 let extract_ids ids lfun accu =
   let fold id v accu =
-    let v = Value.normalize v in
     if has_type v (topwit wit_intro_pattern) then
       let (_, ipat) = out_gen (topwit wit_intro_pattern) v in
       if Id.List.mem id ids then accu
@@ -816,7 +809,6 @@ let interp_constr_may_eval ist env sigma c =
 
 (** TODO: should use dedicated printers *)
 let message_of_value v =
-  let v = Value.normalize v in
   let pr_with_env pr =
     Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in
   let open Genprint in
@@ -986,7 +978,6 @@ let interp_destruction_arg ist gl arg =
       try
         (** FIXME: should be moved to taccoerce *)
         let v = Id.Map.find id ist.lfun in
-        let v = Value.normalize v in
         if has_type v (topwit wit_intro_pattern) then
           let v = out_gen (topwit wit_intro_pattern) v in
           match v with
@@ -1248,7 +1239,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       Ftactic.run args tac
 
 and force_vrec ist v : Val.t Ftactic.t =
-  let v = Value.normalize v in
   if has_type v (topwit wit_tacvalue) then
     let v = to_tacvalue v in
     match v with
@@ -1324,7 +1314,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
 and interp_app loc ist fv largs : Val.t Ftactic.t =
   let (>>=) = Ftactic.bind in
   let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
-  let fv = Value.normalize fv in
   if has_type fv (topwit wit_tacvalue) then
   match to_tacvalue fv with
      (* if var=[] and body has been delayed by val_interp, then body
@@ -1377,7 +1366,6 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
 
 (* Gives the tactic corresponding to the tactic value *)
 and tactic_of_value ist vle =
-  let vle = Value.normalize vle in
   if has_type vle (topwit wit_tacvalue) then
   match to_tacvalue vle with
   | VFun (appl,trace,lfun,[],t) ->
@@ -1604,7 +1592,6 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
   Ftactic.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = project gl in
-  let result = Value.normalize result in
   try
     let cresult = coerce_to_closed_constr env result in
     Proofview.tclLIFT begin
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f7a3789a21..788e4d268a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1044,7 +1044,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
+    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 34df7d3d72..78e6bc6f14 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -275,7 +275,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 
 let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite
+  | Some (Some _) -> mib.mind_finite == BiFinite
   | _ -> true
 
 (* Annotation for cases *)
@@ -486,7 +486,7 @@ let find_inductive env sigma c =
   let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
-        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
+        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> CoFinite ->
         let l = List.map EConstr.Unsafe.to_constr l in
         (ind, l)
     | _ -> raise Not_found
@@ -496,7 +496,7 @@ let find_coinductive env sigma c =
   let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
-        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
+        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == CoFinite ->
         let l = List.map EConstr.Unsafe.to_constr l in
         (ind, l)
     | _ -> raise Not_found
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bbb3a1bb2b..bc9990d026 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -65,7 +65,7 @@ type typeclass = {
   cl_impl : global_reference;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (global_reference * bool) option list * Context.Rel.t;
+  cl_context : global_reference option list * Context.Rel.t;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Context.Rel.t;
@@ -175,7 +175,7 @@ let subst_class (subst,cl) =
   and do_subst_gr gr = fst (subst_global subst gr) in
   let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in
   let do_subst_context (grs,ctx) =
-    List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
+    List.smartmap (Option.smartmap do_subst_gr) grs,
     do_subst_ctx ctx in
   let do_subst_projs projs = List.smartmap (fun (x, y, z) -> 
     (x, y, Option.smartmap do_subst_con z)) projs in
@@ -213,10 +213,10 @@ let discharge_class (_,cl) =
       let newgrs = List.map (fun decl ->
 			     match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with
 			     | None -> None
-			     | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
+                             | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
 			    ctx'
       in
-      List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+      List.smartmap (Option.smartmap Lib.discharge_global) grs
       @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 8ee061330a..0cbe1c71c0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -25,9 +25,8 @@ type typeclass = {
   cl_impl : global_reference;
 
   (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
-     The boolean indicates if the typeclass argument is a direct superclass and the global reference
-     gives a direct link to the class itself. *)
-  cl_context : (global_reference * bool) option list * Context.Rel.t;
+      The global reference gives a direct link to the class itself. *)
+  cl_context : global_reference option list * Context.Rel.t;
 
   (** Context of definitions and properties on defs, will not be shared *)
   cl_props : Context.Rel.t;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 30674fee27..b41fb4e4dd 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -666,7 +666,7 @@ let is_eta_constructor_app env sigma ts f l1 term =
   | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite &&
+      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
           Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
 	(** Check that the other term is neutral *)
 	is_neutral env sigma ts term
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 647111bbe1..2b7886d115 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -235,8 +235,8 @@ let print_type_in_type ref =
 let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
     let eta = match recflag with
-    | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion"
-    | Decl_kinds.BiFinite -> str " with eta conversion"
+    | CoFinite | Finite -> str" without eta conversion"
+    | BiFinite -> str " with eta conversion"
     in
     [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
   | _ -> []
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 05292b06ba..fb9d45a793 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -125,7 +125,7 @@ let print_mutual_inductive env mind mib udecl =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
   in
   let keyword =
-    let open Decl_kinds in
+    let open Declarations in
     match mib.mind_finite with
     | Finite -> "Inductive"
     | BiFinite -> "Variant"
@@ -184,7 +184,7 @@ let print_record env mind mib udecl =
       (Array.to_list (Univ.Instance.to_array u)) udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let keyword =
-    let open Decl_kinds in
+    let open Declarations in
     match mib.mind_finite with
     | BiFinite -> "Record"
     | Finite -> "Inductive"
@@ -346,7 +346,7 @@ let print_body is_impl env mp (l,body) =
         pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
       with e when CErrors.noncritical e ->
         let keyword =
-          let open Decl_kinds in
+          let open Declarations in
           match mib.mind_finite with
           | Finite -> def "Inductive"
           | BiFinite -> def "Variant"
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 2c8ca19722..a3a3e0a9e9 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -48,7 +48,7 @@ let match_with_non_recursive_type sigma t =
         let (hdapp,args) = decompose_app sigma t in
         (match EConstr.kind sigma hdapp with
            | Ind (ind,u) ->
-               if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then
+               if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then
 		 Some (hdapp,args)
 	       else
 		 None
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 508040ec18..4ee0a8a7b2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1492,7 +1492,7 @@ let simplest_ecase c = general_case_analysis true None (c,NoBindings)
 
 exception IsNonrec
 
-let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Decl_kinds.BiFinite
+let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite
 
 let find_ind_eliminator ind s gl =
   let gr = lookup_eliminator ind s in
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index b1769da3d8..31bc1cc31d 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -165,13 +165,13 @@ End Backport_WSets.
 (** * From new Sets to new ones *)
 
 Module Backport_Sets
- (E:OrderedType.OrderedType)
- (M:MSetInterface.Sets with Definition E.t := E.t
-                       with Definition E.eq := E.eq
-                       with Definition E.lt := E.lt)
- <: FSetInterface.S with Module E:=E.
+ (O:OrderedType.OrderedType)
+ (M:MSetInterface.Sets with Definition E.t := O.t
+                       with Definition E.eq := O.eq
+                       with Definition E.lt := O.lt)
+ <: FSetInterface.S with Module E:=O.
 
-  Include Backport_WSets E M.
+  Include Backport_WSets O M.
 
   Implicit Type s : t.
   Implicit Type x y : elt.
@@ -182,21 +182,21 @@ Module Backport_Sets
   Definition min_elt_1 : forall s x, min_elt s = Some x -> In x s
    := M.min_elt_spec1.
   Definition min_elt_2 : forall s x y,
-   min_elt s = Some x -> In y s -> ~ E.lt y x
+   min_elt s = Some x -> In y s -> ~ O.lt y x
    := M.min_elt_spec2.
   Definition min_elt_3 : forall s, min_elt s = None -> Empty s
    := M.min_elt_spec3.
   Definition max_elt_1 : forall s x, max_elt s = Some x -> In x s
    := M.max_elt_spec1.
   Definition max_elt_2 : forall s x y,
-   max_elt s = Some x -> In y s -> ~ E.lt x y
+   max_elt s = Some x -> In y s -> ~ O.lt x y
    := M.max_elt_spec2.
   Definition max_elt_3 : forall s, max_elt s = None -> Empty s
    := M.max_elt_spec3.
-  Definition elements_3 : forall s, sort E.lt (elements s)
+  Definition elements_3 : forall s, sort O.lt (elements s)
    := M.elements_spec2.
   Definition choose_3 : forall s s' x y,
-   choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y
+   choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y
    := M.choose_spec3.
   Definition lt_trans : forall s s' s'', lt s s' -> lt s' s'' -> lt s s''
    := @StrictOrder_Transitive _ _ M.lt_strorder.
@@ -211,7 +211,7 @@ Module Backport_Sets
     [ apply EQ | apply LT | apply GT ]; auto.
   Defined.
 
-  Module E := E.
+  Module E := O.
 
 End Backport_Sets.
 
@@ -342,13 +342,13 @@ End Update_WSets.
 (** * From old Sets to new ones. *)
 
 Module Update_Sets
- (E:Orders.OrderedType)
- (M:FSetInterface.S with Definition E.t := E.t
-                    with Definition E.eq := E.eq
-                    with Definition E.lt := E.lt)
- <: MSetInterface.Sets with Module E:=E.
+ (O:Orders.OrderedType)
+ (M:FSetInterface.S with Definition E.t := O.t
+                    with Definition E.eq := O.eq
+                    with Definition E.lt := O.lt)
+ <: MSetInterface.Sets with Module E:=O.
 
-  Include Update_WSets E M.
+  Include Update_WSets O M.
 
   Implicit Type s : t.
   Implicit Type x y : elt.
@@ -359,21 +359,21 @@ Module Update_Sets
   Definition min_elt_spec1 : forall s x, min_elt s = Some x -> In x s
    := M.min_elt_1.
   Definition min_elt_spec2 : forall s x y,
-   min_elt s = Some x -> In y s -> ~ E.lt y x
+   min_elt s = Some x -> In y s -> ~ O.lt y x
    := M.min_elt_2.
   Definition min_elt_spec3 : forall s, min_elt s = None -> Empty s
    := M.min_elt_3.
   Definition max_elt_spec1 : forall s x, max_elt s = Some x -> In x s
    := M.max_elt_1.
   Definition max_elt_spec2 : forall s x y,
-   max_elt s = Some x -> In y s -> ~ E.lt x y
+   max_elt s = Some x -> In y s -> ~ O.lt x y
    := M.max_elt_2.
   Definition max_elt_spec3 : forall s, max_elt s = None -> Empty s
    := M.max_elt_3.
-  Definition elements_spec2 : forall s, sort E.lt (elements s)
+  Definition elements_spec2 : forall s, sort O.lt (elements s)
    := M.elements_3.
   Definition choose_spec3 : forall s s' x y,
-   choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y
+   choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y
    := M.choose_3.
 
   Instance lt_strorder : StrictOrder lt.
@@ -407,6 +407,6 @@ Module Update_Sets
   Lemma compare_spec : forall s s', CompSpec eq lt s s' (compare s s').
   Proof. intros; unfold compare; destruct M.compare; auto. Qed.
 
-  Module E := E.
+  Module E := O.
 
 End Update_Sets.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 2feaaa04cd..b7a62a78c0 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -27,16 +27,8 @@ let rec print_prefix_list sep = function
   | x :: l -> print sep; print x; print_prefix_list sep l
   | [] -> ()
 
-let usage () =
-  output_string stderr "Usage summary:\
-\n\
-\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
-\n  ... [any] ... [-extra[-phony] result dependencies command]\
-\n  ... [-I dir] ... [-R physicalpath logicalpath]\
-\n  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
-\n  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
-\n  [-h] [--help]\
-\n\
+let usage_common () =
+  output_string stderr "\
 \n[file.v]: Coq file to be compiled\
 \n[file.ml[i4]?]: Objective Caml file to be compiled\
 \n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
@@ -65,10 +57,29 @@ let usage () =
 \n[-install opt]: where opt is \"user\" to force install into user directory,\
 \n  \"none\" to build a makefile with no install target or\
 \n  \"global\" to force install in $COQLIB directory\
+\n[-bypass-API]: when compiling plugins, bypass Coq API\
+\n"
+
+let usage_coq_project () =
+  output_string stderr "Available arguments:";
+  usage_common ();
+  exit 1
+
+let usage_coq_makefile () =
+  output_string stderr "Usage summary:\
+\n\
+\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
+\n  ... [any] ... [-extra[-phony] result dependencies command]\
+\n  ... [-I dir] ... [-R physicalpath logicalpath]\
+\n  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
+\n  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
+\n  [-h] [--help]\
+\n";
+  usage_common ();
+  output_string stderr "\
 \n[-f file]: take the contents of file as arguments\
-\n[-o file]: output should go in file file\
+\n[-o file]: output should go in file file (recommended)\
 \n	Output file outside the current directory is forbidden.\
-\n[-bypass-API]: when compiling plugins, bypass Coq API\
 \n[-h]: print this usage summary\
 \n[--help]: equivalent to [-h]\n";
   exit 1
@@ -380,8 +391,8 @@ let share_prefix s1 s2 =
   | _ -> false
 
 let _ =
+  let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
   let prog, args =
-    if Array.length Sys.argv = 1 then usage ();
     let args = Array.to_list Sys.argv in
     let prog = List.hd args in
     prog, List.tl args in
@@ -392,7 +403,7 @@ let _ =
 
   let project = 
     try cmdline_args_to_project ~curdir:Filename.current_dir_name args
-    with Parsing_error s -> prerr_endline s; usage () in
+    with Parsing_error s -> prerr_endline s; usage_coq_project () in
 
   if only_destination <> None then begin
     destination_of project (Option.get only_destination);
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 51dd5cd4f5..ec6b62ee27 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -317,7 +317,7 @@ let build_beq_scheme mode kn =
       let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
 	if not (Sorts.List.mem InSet kelim) then
 	  raise (NonSingletonProp (kn,i));
-        if mib.mind_finite = Decl_kinds.CoFinite then
+        if mib.mind_finite = CoFinite then
 	  raise NoDecidabilityCoInductive;
         let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
         create_input fix),
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c2e9a5ab44..6914f899b7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -141,7 +141,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
 	  (fun avoid (clname, _) ->
 	    match clname with
-	    | Some (cl, b) ->
+            | Some cl ->
 		let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 883121479f..d376696f76 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -11,7 +11,6 @@ open Util
 open Constr
 open Environ
 open Entries
-open Termops
 open Redexpr
 open Declare
 open Constrintern
@@ -49,55 +48,57 @@ let warn_implicits_in_term =
           strbrk "Implicit arguments declaration relies on type." ++ spc () ++
             strbrk "The term declares more implicits than the type here.")
 
+let check_imps ~impsty ~impsbody =
+  let b =
+    try
+      List.for_all (fun (key, (va:bool*bool*bool)) ->
+          (* Pervasives.(=) is OK for this type *)
+          Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va)
+        impsbody
+    with Not_found -> false
+  in
+  if not b then warn_implicits_in_term ()
+
 let interp_definition pl bl poly red_option c ctypopt =
+  let open EConstr in
   let env = Global.env() in
+  (* Explicitly bound universes and constraints *)
   let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  (* Build the parameters *)
   let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
-  let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
-  let nb_args = Context.Rel.nhyps ctx in
-  let evd,imps,ce =
-    match ctypopt with
-      None ->
-        let evd, subst = Evd.nf_univ_variables evd in
-        let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
-        let env_bl = push_rel_context ctx env in
-        let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in
-        let c = EConstr.Unsafe.to_constr c in
-        let evd,nf = Evarutil.nf_evars_and_universes evd in
-        let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
-        let evd = Evd.restrict_universe_context evd vars in
-        let uctx = Evd.check_univ_decl ~poly evd decl in
-        evd, imps1@(Impargs.lift_implicits nb_args imps2),
-          definition_entry ~univs:uctx body
-    | Some ctyp ->
-        let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in
-        let evd, subst = Evd.nf_univ_variables evd in
-        let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
-        let env_bl = push_rel_context ctx env in
-        let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
-        let c = EConstr.Unsafe.to_constr c in
-        let evd, nf = Evarutil.nf_evars_and_universes evd in
-        let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let ty = EConstr.Unsafe.to_constr ty in
-        let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in
-        let beq b1 b2 = if b1 then b2 else not b2 in
-        let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in
-        (* Check that all implicit arguments inferable from the term
-           are inferable from the type *)
-        let chk (key,va) =
-          impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *)
-        in
-        if not (try List.for_all chk imps2 with Not_found -> false)
-        then warn_implicits_in_term ();
-        let bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
-        let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in
-        let vars = Univ.LSet.union bodyvars tyvars in
-        let evd = Evd.restrict_universe_context evd vars in
-        let uctx = Evd.check_univ_decl ~poly evd decl in
-        evd, imps1@(Impargs.lift_implicits nb_args impsty),
-          definition_entry ~types:typ ~univs:uctx body
+  (* Build the type *)
+  let evd, tyopt = Option.fold_left_map
+      (interp_type_evars_impls ~impls env_bl)
+      evd ctypopt
+  in
+  (* Build the body, and merge implicits from parameters and from type/body *)
+  let evd, c, imps, tyopt =
+    match tyopt with
+    | None ->
+      let evd, (c, impsbody) = interp_constr_evars_impls ~impls env_bl evd c in
+      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
+    | Some (ty, impsty) ->
+      let evd, (c, impsbody) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
+      check_imps ~impsty ~impsbody;
+      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
+  in
+  (* universe minimization *)
+  let evd = Evd.nf_constraints evd in
+  (* Substitute evars and universes, and add parameters.
+     Note: in program mode some evars may remain. *)
+  let ctx = List.map (EConstr.to_rel_decl evd) ctx in
+  let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
+  let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in
+  (* Keep only useful universes. *)
+  let uvars_fold uvars c =
+    Univ.LSet.union uvars (universes_of_constr env evd (of_constr c))
   in
+  let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
+  let evd = Evd.restrict_universe_context evd uvars in
+  (* Check we conform to declared universes *)
+  let uctx = Evd.check_univ_decl ~poly evd decl in
+  (* We're done! *)
+  let ce = definition_entry ?types:tyopt ~univs:uctx c in
   (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
 
 let check_definition (ce, evd, _, imps) =
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f3f50f41dd..1c8677e9cd 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -25,7 +25,6 @@ open Nametab
 open Impargs
 open Reductionops
 open Indtypes
-open Decl_kinds
 open Pretyping
 open Evarutil
 open Indschemes
@@ -411,7 +410,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
   (* spiwack: raises an error if the structure is supposed to be non-recursive,
         but isn't *)
   begin match mie.mind_entry_finite with
-  | BiFinite when is_recursive mie ->
+  | Declarations.BiFinite when is_recursive mie ->
       if Option.has_some mie.mind_entry_record then
         user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
       else
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e4ca98749c..2f4c95affc 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -258,7 +258,7 @@ let declare_one_induction_scheme ind =
 
 let declare_induction_schemes kn =
   let mib = Global.lookup_mind kn in
-  if mib.mind_finite <> Decl_kinds.CoFinite then begin
+  if mib.mind_finite <> Declarations.CoFinite then begin
     for i = 0 to Array.length mib.mind_packets - 1 do
       declare_one_induction_scheme (kn,i);
     done;
@@ -268,7 +268,7 @@ let declare_induction_schemes kn =
 
 let declare_eq_decidability_gen internal names kn =
   let mib = Global.lookup_mind kn in
-  if mib.mind_finite <> Decl_kinds.CoFinite then
+  if mib.mind_finite <> Declarations.CoFinite then
     ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
 
 let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
@@ -512,7 +512,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
 let declare_default_schemes kn =
   let mib = Global.lookup_mind kn in
   let n = Array.length mib.mind_packets in
-  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag)
+  if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag)
      && mib.mind_typing_flags.check_guarded then
     declare_induction_schemes kn;
   if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 27a680b9b6..6ef310837c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -100,7 +100,7 @@ let find_mutually_recursive_statements sigma thms =
           match EConstr.kind sigma t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite ->
+                mind.mind_finite <> Declarations.CoFinite ->
               [ind,x,i]
           | _ ->
               []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in
@@ -110,7 +110,7 @@ let find_mutually_recursive_statements sigma thms =
         match EConstr.kind sigma whnf_ccl with
         | Ind ((kn,_ as ind),u) when
               let mind = Global.lookup_mind kn in
-              Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
+              Int.equal mind.mind_ntypes n && mind.mind_finite == Declarations.CoFinite ->
             [ind,x,0]
         | _ ->
             [] in
diff --git a/vernac/record.ml b/vernac/record.ml
index 114b55cb40..d9dc16d96e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -143,7 +143,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
   let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
   let assums = List.filter is_local_assum newps in
   let params = List.map (RelDecl.get_name %> Name.get_id) assums in
-  let ty = Inductive (params,(finite != BiFinite)) in
+  let ty = Inductive (params,(finite != Declarations.BiFinite)) in
   let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in
   let env2,sigma,impls,newfs,data =
     interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
@@ -507,7 +507,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
          | Monomorphic_const_entry univs ->
            Monomorphic_ind_entry univs
        in
-       let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
+       let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -523,7 +523,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
   let ctx_context =
     List.map (fun decl ->
       match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with
-      | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
+      | Some (_, ((cl,_), _)) -> Some cl.cl_impl
       | None -> None)
       params, params
   in