bwaa, a Pervasive.compare

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16543 85f007b7-540e-0410-9357-904b9bb8a0f7
Why not going inside fixpoint definition with appcontext ?

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16545 85f007b7-540e-0410-9357-904b9bb8a0f7
Do not compute fallback eagerly in Evarconv

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16546 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing a useless location in ltac trace mechanism.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16547 85f007b7-540e-0410-9357-904b9bb8a0f7
Modest protection against "injection" and co raising anomaly in
-nois mode.  This is not perfect yet. E.g. "injection" used while
before eq is defined while compiling Logic.v would raise an anomaly.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16548 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing buggy backtracking in "intros * pat" with failing "pat".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16549 85f007b7-540e-0410-9357-904b9bb8a0f7
Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an
"injection" tactic when applied on an equality statement. Moreover,
hypotheses are now entered in the left-to-right order.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16550 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing a typo in the documentation of discriminate.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16551 85f007b7-540e-0410-9357-904b9bb8a0f7
Flags V8_4 for compatibility infrastructure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16555 85f007b7-540e-0410-9357-904b9bb8a0f7
Making the behavior of "injection ... as ..." more natural:
- hypotheses are introduced in the left-to-right order
- intropatterns have to match the number of generated hypotheses, and,
  if less, new introduction names are automatically generated
- clearing the hypothesis on which injection is applied, if any.

However, this is a source of incompatibilities (for a variant of
injection that is hopefully not used a lot). Compatibility can be
restored by "Unset Injection L2R Pattern Order".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7
A constructive proof of Fan theorem where paths are represented by predicates.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7
Start documenting new [rewrite_strat] tactic that applies rewriting
according to a given strategy.
- Enhance the hints/lemmas strategy to support "using tac" comming from
rewrite hints to solve side-conditions.  


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16558 85f007b7-540e-0410-9357-904b9bb8a0f7
Backtrack on unneeded change of interface for pose_metas_as_evars.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16559 85f007b7-540e-0410-9357-904b9bb8a0f7
Use a Summary.ref for the tactic in tactic options for proper backtracking
and handling of locality (fixes FingerTree contrib).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16560 85f007b7-540e-0410-9357-904b9bb8a0f7
Replacing lists by maps in matching interpretation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16561 85f007b7-540e-0410-9357-904b9bb8a0f7
Add an option to shrink the context of program obligations to avoid
unnecessary dependencies (applies to obligations defined by tactics
only). Satisfies RFE #1984.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16562 85f007b7-540e-0410-9357-904b9bb8a0f7
Document changes and add missing documentation for Program options.


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

Now, instead of having three unrelated types describing a dynamic
type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type"
whose parameters describe the reified type at each level.

This has various advantages:

- No more code duplication to handle the three level separately;
- Safer code: one is not authorized to mix unrelated types when what
was morally expected was a genarg_type.
- Each level-specialized representation can be accessed through
well-typed projections: rawwit, glbwit and topwit.

Documenting a bit Genarg b.t.w.

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