Optimizing universes: tail-rec, allocation friendly [compare_leq].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16946 85f007b7-540e-0410-9357-904b9bb8a0f7
Allocation-friendly version of [Pre_env.push_named].

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16948 85f007b7-540e-0410-9357-904b9bb8a0f7
Printing heap on every processed sentence.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16949 85f007b7-540e-0410-9357-904b9bb8a0f7
Profile only when CAMLRUNPARAM is set.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16950 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert the two last commits. My bad, I messed up git-svn commands...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16951 85f007b7-540e-0410-9357-904b9bb8a0f7
[Reductionops.append_stack_app]: do not allocate a useless array.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16952 85f007b7-540e-0410-9357-904b9bb8a0f7
Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16953 85f007b7-540e-0410-9357-904b9bb8a0f7
Do not generate useless argument arrays in whd_* functions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
Useless array-to-list casts in Unification.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16955 85f007b7-540e-0410-9357-904b9bb8a0f7
Optimization in unification: when checking that the head of a term is an
evar or a meta, don't reconstruct the whole term. This hopefully saves
a lot of useless allocations and computing time.

I may have slightly changed the heuristic though, as only evars in front of
applications where recognized as such, whereas now this pass through cases
and fixpoints. I am walking on thin ice, but the test-suite was OK...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16956 85f007b7-540e-0410-9357-904b9bb8a0f7
More efficient implementation of [Evd.retract_coercible_metas].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16957 85f007b7-540e-0410-9357-904b9bb8a0f7
Various optimizations of Evd.meta_* functions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16958 85f007b7-540e-0410-9357-904b9bb8a0f7
Avoiding useless allocations in Closure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16959 85f007b7-540e-0410-9357-904b9bb8a0f7
Efficient filtered functions in Evd. We test that a filter is actually
different from the identity before trying to compute filtered env/hyps.

According to profiling, it seems that the filter operation is NEVER taken,
that is, all filters that reach toplevel are dummy. There is surely something
to do here...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16960 85f007b7-540e-0410-9357-904b9bb8a0f7
Conv_orable made functional and part of pre_env

But for vm, the kernel should be functional now

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: scroll to the right position if there is an interp error

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16962 85f007b7-540e-0410-9357-904b9bb8a0f7
Future: better doc + restore ~pure optimization

This optimization was undone because the kernel type checking was
not a pure functions (it was accessing the conv_oracle state imperatively).
Now that the conv_oracle state is part of env, the optimization can be
restored.  This was the cause of the increase in memory consumption, since
it was forcing to keep a copy of the system state for every proof, even the
ones that are not delayed/delegated to slaves.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing Kerpair.hash. Since the beginning, it dit not respect the type
equality, maybe impeding hashconsing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16964 85f007b7-540e-0410-9357-904b9bb8a0f7
Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)

 This commit should fix the contrib ProjectiveGeometry

 This update_delta_resolver is in fact a sequential composition
 (resolver1 then resolver2). The earlier version was strangely
 favoring the bindings coming from resolver2 over the bindings
 coming from (resolver1 chained with resolver2). So any inlining
 information stored in resolver1 could be discarded savagely.
 Apparently, this situation wasn't occurring in practice until
 recently, when I started to do lots of Mod_subst.join for
 improving the size of modular libobjects in the vo's.

 So, when combining two resolvers now :

 - Inline(_,None) is the weakest information, it's just a
   declaration that we intend to inline this kn someday if possible
   (i.e. when we'll have a transparent implementation for it).
   This kind of Inline is only relevant inside a module type.

 - Equiv(_) should only appear in modules (after some Include)
   so it should be ok if it takes precedence over any Inline(_,None)
   remaining in the other resolver.

 - Inline(_,Some _) is there after functor application
   (cf inline_delta_resolver) : we've done the inlining,
   so we don't care anymore about other Equiv(_) or Inline(_,None)
   informations about this kn, since we have anyway a new body
   for it.

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