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 *)