Add an init_setoid check in rewrite to avoid trying to get undefined references.
Fixes the behavior of reflexivity/symmetry etc... when Setoid is not loaded.
Fast path in Canonical structure detection. We do not always compute the normal
form of a potential canonical argument anymore, and we check that it may be part
of a canonical structure first.
More open in base_include
Small short optimization of instantiation in Evd.
Updating CHANGES w.r.t. opacity in type inference + layout of file.
Typo in stm error message.
Made the subterm finding function make_abstraction independent of the
proof engine. Moved it to unification.ml.
Extra check for indirect dependency when abstracting a term which is
not a variable, in the future objective to factorize code between
"generalize dependent" and "set", "destruct", etc.
Moved code for finding subterms (pattern, induction, set, generalize, ...)
into a specific new cleaned file find_subterm.ml.

This makes things clearer but also solves some dependencies problem
between Evd, Termops and Pretype_errors.
Quickly fixing bug #2996: typing functions now check when referring to
a global reference that the current (goal) env contains all the
section variables that the global reference expects to be present.

Note that the test for inclusion might be costly: everytime a
conversion happens in a section variable copied in a goal, this
conversion has to be redone when referring to a constant dependent on
this section variable.

It is unclear to me whether we should not instead give global names to
section variables so that they exist even if they are not listed in
the context of the current goal.

Here are two examples which are still problematic:
Section A.
Let B := True : Type.
Definition C := eq_refl : B = True.
Theorem D : Type.
clearbody B.
set (x := C).
unfold C in x.
(* inconsistent context *)

or

Section A.
Let B : Type.
exact True.
Qed.
Definition C := eq_refl : B = True.  (* Note that this violated the Qed. *)
Theorem D : Type.
set (x := C).
unfold C in x.
(* inconsistent context *)
Small refinement about whether it is tolerated for compatibility that
or-and intropatterns bind a limited number of patterns: if * or ** are
used, the bound has to be used (since there is no heavy compatibility
to respect for * and **). This fixes test-suite/success/intros.v.
Quick fix of bug #2996 continued (case of inductive types).
Move Params definition in generalize rewriting out of a section so that
its universe doesn't get constrained unnecessarily (bug found in MathClasse).
Also avoid using rewrite itself in a proof in Morphisms.
Really honor the [simpl never] flag in whd_simpl, it was still doing reductions in
case the constant was hiding a direct match for example. Also avoid two lookups
of ReductionBehavior per constant application in simpl.
When building on-the-fly elimination principles, set the predicates universe variable
as algebraic so it can disappear from the proof (it always gets substituted away from
the term). This means less spurious universes remaining in proof terms.
Coq_makefile: -extra[-phony] correction + doc
Coqdep: update include strategies

-I is (only) the ml one
-I -as is fixed
-Q is understood
-R is not a recursive ml include anymore

$COQENV, user_contrib, ... are not recursively included

coqlib/theories and coqlib/plugins are still recursively included (for now). (This
may deserves an option)

Closes Bug 2910: If there is a "Require a." in a b.v and a a.vo in path but no a.v,
coqdep does not complains about a missing a.v.
coqc is -Q aware
Coq_makefile takes advantages of -I -Q -R cleanup
refresh INSTALL