Fixing vm_compute bug #2729 (function used to decompose constructors
did not handle let-ins and was wrongly specified). Thanks to Pierre
Boutillier and Pierre-Marie Pédrot for pointing out the source of the
bug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
A bit of cleaning: unifying push_rels and push_rel_context.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15031 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove support for "abstract typing constraints" that requires unicity of solutions to unification.
Only allow bidirectional checking of constructor applications, enabled by a program_mode flag:
it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated
with delta-equivalent but not syntactically equivalent terms.
Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
Second step of integration of Program:
- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
Integrated obligations/eterm and program well-founded fixpoint building to toplevel/
The code is not called yet from there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15035 85f007b7-540e-0410-9357-904b9bb8a0f7
Final part of moving Program code inside the main code. Adapted add_definition/fixpoint and parsing of the "Program" prefix.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15037 85f007b7-540e-0410-9357-904b9bb8a0f7
Revise API of understand_ltac to be parameterized by a flag for resolution of evars.
Used when interpreting a constr in Ltac: resolution is now launched if the constr
is casted.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15039 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix merge and add missing file.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15040 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing bug #2732 (anomaly when using the tolerance for writing
"f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an
Ltac function - see Tacinterp.add_primitive_tactic).

More precisely, when parsing "f ref" and "ref" is recognized as the
name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic
(like "eauto", "firstorder", "discriminate", ...), the code was
correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END'
was given (where "foo" has no arguments in the rule) but not when a rule
of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given
(where "foo" had an optional argument in the rule). In particular,
"firstorder" was in this case.

More generally, if, for an extra argument able to parse the empty string, a rule
`TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given,
then "foo" was not recognized as parseable as an atomic string (this
happened e.g. for "eauto").  This is now also fixed.

There was also another bug when the internal name of tactic was not
the same as the user-level name of the tactic. This is the reason why
"congruence" was not recognized when given as argument of an ltac (its
internal name is "cc").

Incidentally removed the redundant last line in the parsing rule for
"firstorder".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15041 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing redundant entry int_nelist and removing extra space when
printing occurrences list.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15044 85f007b7-540e-0410-9357-904b9bb8a0f7
Yet another subtlety with bug 2732: when several grammar rules of a
TACTIC EXTEND block possibly parse the stand-alone name of a tactic,
then only the first rule must be registered in the atomic tactic table
so as to be consistent with what happens when the tactic is invoked
directly via its parsing rules and not via the interpretation of a
reference in the atomic tactic table. Concretely, this affects TACTIC
EXTEND blocks of the form

TACTIC EXTEND foo
  [ "bar" tactic_opt(tac) -> ... ]
| [ "bar" constr_list(tac) -> ... ]

where both rules parses "bar" alone but only the first rule must be
registered in the atomic table,

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15046 85f007b7-540e-0410-9357-904b9bb8a0f7
Arguments/simpl: allow ! even on non fixpoints

It is now possible to tell simpl to unfold a constant
that hides no "match" but is applied to concrete arguments.

Arguments id _ !n.
Goal forall x, id x = id 2.
intros; simpl.

x : nat
========
id x = 2

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15048 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixes bug: #2692 (Arguments/simpl off by 1)

simpl was accessing the reduction stack at position n when
the length of the stack was exactly n.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15049 85f007b7-540e-0410-9357-904b9bb8a0f7
RefMan: Environment variables description update

There is no mention in the refman of relative search of the lib from the binaries directory and of the use of _CoqProject by CoqIdE.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15052 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 2709: Duplication in coqdoc index entries

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15053 85f007b7-540e-0410-9357-904b9bb8a0f7
Hopefully complying with camlp5 < 6.00 syntax

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15055 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix bugs related to Program integration.
- reinstall (x : T | P) binder syntax extension.
- fix a wrong Evd.define in coercion code.
- Simplify interface of eterm_obligations to take a single evar_map.
- Fix a slightly subtle bug related to resolvability of evars: some
were marked unresolvable and never set back to resolvable across calls
to typeclass resolution.

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