Update debug code according to reorganization into modules.


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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16255 85f007b7-540e-0410-9357-904b9bb8a0f7
More informative error when a global reference is used in a context of
local variables which is a different from the one of its definition. E.g.:

Section A.
Variable n:nat.
Definition c:=n.
Goal True.
clear n.
Check c.

[I'm however unsure that "n" should not continue to be accessible via
some global (qualified) name, even after the "clear n".]

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16256 85f007b7-540e-0410-9357-904b9bb8a0f7
Repairing r16205: errors raised by check_evar_instance were no longer
trapped by solve_simple_eqn.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16257 85f007b7-540e-0410-9357-904b9bb8a0f7
compare_stack_shape before ise_stack2 in evar_conv

+ revert r16130

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

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

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

This makes pr_module_vardecls side effect free, as any pp function should be

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16261 85f007b7-540e-0410-9357-904b9bb8a0f7
catch failures of pr_vernac to make -time failsafe

Printing Ltac code is broken. This was not compiling with -time

  Ltac pop_succn e := eval lazy beta iota delta [plus] in (1 + 1).

The bug in the pretty printer should be fixed too...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16262 85f007b7-540e-0410-9357-904b9bb8a0f7
Added a Local Definition vernacular command. This type of definition
has to be refered through its qualified name even when the module
containing it is imported.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
Documentation of the "Local Definition" command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16264 85f007b7-540e-0410-9357-904b9bb8a0f7
Obligations generated by Program are now local.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16265 85f007b7-540e-0410-9357-904b9bb8a0f7
Allowing (Co)Fixpoint to be defined local and Let-style.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
Allowing different types of, not to be mixed, generic Stores through
functor application. Rewritten the interface btw.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16267 85f007b7-540e-0410-9357-904b9bb8a0f7
Updated Exninfo to the new Store type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7
New function Errors.noncritical for restricting try ... with ...

 For the moment, are considered critical :

  Sys.Break, Stack_overflow, Out_of_memory
  Assert_failure, Match_failure, Anomaly, Timeout, Drop, Exit

 These exceptions should normally *not* be catched by a "try",
 hence the suggested code for generic "try":

  try ... with e when Errors.noncritical e -> ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16269 85f007b7-540e-0410-9357-904b9bb8a0f7
invalid_arg instead of raise (Invalid_argement ...)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
Term.dest* functions now raise specific DestKO exn instead of Invalid_argument

**Warning** the ml code of plugins may have to be adapted after this.

Concerning coq itself, I've done the adaptations, let's hope I've
forgotten none. In practice, the number of changes are relatively low,
and the code is quite cleaner this way.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16271 85f007b7-540e-0410-9357-904b9bb8a0f7
Recdef: an anomaly isn't so anomalous, occurs in 1618.v

 For the moment, this anomaly is catched and ignore later,
 but that will changed soon.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16272 85f007b7-540e-0410-9357-904b9bb8a0f7
Equality: avoid an anomaly about inj_pair2_eq_dec

 In coming commits, we'll restrict (try ... with ...), in particular
 to avoid catching anomalies. Currently, an anomaly about inj_pair2_eq_dec
 is raised and catched, let's avoid that by ensuring that Eqdep_dec is
 loaded before entering the critical code.

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