More functional implementation of locality_flag and program_mode

This commit introduces 2 new vernac_expr constructors:
- VernacLocal (b,v)  that represents a vernacular v with the "Local" modifier
- VernacProgram v    that represents a vernacular v with the "Program" modifier

This allows the parser to avoid using side effects to model the two
modifiers, that are now represented in the AST.  This also decouples the
parsing phase from the interpretation phase, since parsing a second
phrase does not alter the locality flag for the first phrase.

As a consequence all the locality_flag components of vernac_expr have
been removed, but for the ones that (for retro compatibility) allow
an "infix" Local flag.  In these cases the boolean is renamed
obsolete_locality (as the grammar entry that parses it), and during
interpretation we check that at most one locality flag is specified,
using the idiom (where the input local is the obsolete one):

  let local = enforce_XXX_locality locality local in

Another improvement is that the default locality is not chosen in the
parser, but in the interpreter where the idiom

  let local = make_XXX_locality locality in

is used to default the locality to XXX (module/section/whatever).

Unfortunately not all side effects have been removed:
- Flags.program_mode is still used to signal that we are in program mode
- Locality.LocalityFixme.* functions are used in commands that do not
  have an AST, but are parsed as VernacExtend (see vernacinterp.ml)

I guess one could fix the latter case systematically adding an extra
argument "locality" to commands attached using VERNAC COMMAND EXTEND.

Fixing plugins adding commands that honour "Local" should look like this:

 VERNAC COMMAND EXTEND Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
     set_default_tactic
-      (Locality.use_section_locality ())
+      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (Tacintern.glob_tactic t) ]
 END

In any case the side effects are set/consumed within then interpretation
phase, and not set during the parsing phase and consumed during the
interpretation phase.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16396 85f007b7-540e-0410-9357-904b9bb8a0f7
anew_instance should not consume the locality twice

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16397 85f007b7-540e-0410-9357-904b9bb8a0f7
Checker: regroup all vo-related types in cic.mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
Checker: reified encoding of .vo types in values.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7
Checker: empty sections hardcoded in cb and mind

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16400 85f007b7-540e-0410-9357-904b9bb8a0f7
Checker: get rid of code handling section variables

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16401 85f007b7-540e-0410-9357-904b9bb8a0f7
Checker: vo validation is now done in check.ml (and always)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16402 85f007b7-540e-0410-9357-904b9bb8a0f7
votour: a small tool for guided tours of .vo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16403 85f007b7-540e-0410-9357-904b9bb8a0f7
Checker : a md5-based way to ensure checker/values.ml is always in sync

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16404 85f007b7-540e-0410-9357-904b9bb8a0f7
Checker: vo validation checks the absence of Var/Evar/Meta

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16405 85f007b7-540e-0410-9357-904b9bb8a0f7
Declaremods: drop some useless stuff (slight gain in vo size)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16406 85f007b7-540e-0410-9357-904b9bb8a0f7
Minor simplifications in Declaremods and Safe_typing

 - get_module_substobjs (resp. modtype) without useless mp_from arg
 - no need for the whole Safe_typing.pack_module
 - ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16407 85f007b7-540e-0410-9357-904b9bb8a0f7
More in IArray

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16408 85f007b7-540e-0410-9357-904b9bb8a0f7
Added regression test for bug #3023 which was solved by Matthieu's
commit r16134 (eta was missing in Flexible/Rigid and
SemiFlexible/Rigid conversion problems).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16409 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing #2968. This is quite brittle though, because we are messing
with the exception catching system of Ltac which is not really
known for its safety, so that it may break a few things.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16411 85f007b7-540e-0410-9357-904b9bb8a0f7
Added group properties of eq_refl, eq_sym, eq_trans

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16413 85f007b7-540e-0410-9357-904b9bb8a0f7
Like in r16346, do not filter local definitions (here in the
type-based second-order unification algorithm).

In type-based second-order unification algorithm, protect local
definitions in instances of evars to wrongly be considered as
potentially flexible.

Altogether, this fixes the anomaly in #3003 (even if some additional
work has to be done to improve the resulting error message, see next
commit).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16414 85f007b7-540e-0410-9357-904b9bb8a0f7
Improving error message in explain_cannot_find_well_typed_abstraction:
make head bound variables distinct from the variables in environment,
so that the naming scheme is the same when, say, printing "fun x:B => foo x"
in environment "x:A" (main error with explicit "fun") and when
printing (secondary error in the "reason" message) "foo x" in
environment "x:A, x:B" (i.e. with "fun" discharged in environment).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16415 85f007b7-540e-0410-9357-904b9bb8a0f7
Using Parameter instead of Variable in test-suite/output

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16417 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqc: repair localisation of errors in files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16418 85f007b7-540e-0410-9357-904b9bb8a0f7