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
A version of Univ.check_eq with no anomaly for Evd.set_eq_sort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16274 85f007b7-540e-0410-9357-904b9bb8a0f7
Hipattern : consider jmeq only when Logic.JMeq is loaded

 Otherwise an Anomaly coming from Coqlib.find_reference is raised
 and catched for the moment, but that will change soon.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16275 85f007b7-540e-0410-9357-904b9bb8a0f7
Restrict (try...with...) to avoid catching critical exn (part 1)

 Why? : avoid catching (and probably ignoring) exceptions
 such as Sys.Break, anomalies, assertions, leading to undetected
 bugs and ignored Ctrl-C.

 How? : when the precise exception(s) concerned by the try is
 known, use them explicitely in the "with". Otherwise, let's use
 the pattern "with e when Errors.noncritical e -> "

 Particular case : when an exception is catched and reraised
 immediately after some adjustments, we leave it untouched.
 Simply, for easily identifying these situations later, the name
 of the exception variable is changed to "reraise".

 Please also adopt this coding style. Automatic checks based
 on the "mascot" tool of X. Clerc will be runned regularly.
 If you want to avoid to check a particular try...with, use
 the variable name "any" after the "with".

 All these changes have been tested using the standard library
 and the test-suite, but unfortunately this is far from ensuring
 that coqtop behaves as before. We'll see after the nightly bench...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7
Restrict (try...with...) to avoid catching critical exn (part 2)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16277 85f007b7-540e-0410-9357-904b9bb8a0f7
Restrict (try...with...) to avoid catching critical exn (part 3)

NB: this "try...with" plus the test at the next line
(if !interning_grammar || env.unb then ...)
were actually catching too many errors (for instance
error_not_enough_arguments).

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