Useless array to list conversions in proof/logic.ml.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16942 85f007b7-540e-0410-9357-904b9bb8a0f7
Evar leak in "absurd" tactic.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16943 85f007b7-540e-0410-9357-904b9bb8a0f7
Native compiler: library compilation errors are now non fatal.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16944 85f007b7-540e-0410-9357-904b9bb8a0f7
- install evar printer for debugging
- make unification try canonical structures before expansion as in evar_conv
- add a fast path to evar inversion (patch from B. Ziliani).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16945 85f007b7-540e-0410-9357-904b9bb8a0f7
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