- changing minimal version for OCaml: Coq uses Filename.dirsep that is available from OCaml 3.11.2 (see bug #2707)
- fixing outdated address for Coq Club

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@14986 85f007b7-540e-0410-9357-904b9bb8a0f7
Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)

 In addition to #2683, this also prevent Vernac.End_of_input
 exceptions when a buffer ends with one of the new delimiters -+*{}.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@14990 85f007b7-540e-0410-9357-904b9bb8a0f7
correction of bug 2457

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@14992 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: correct compare_neq (fix #2703)

 The earlier version was a bit too quick to answer <= while strict
 constraints could still appear from remaining universes to explore.
 Typical situation: compare u v when u <= v and u <= w < v.
 Encountering u <= v isn't enough to conclude yet...

 This means that kernels from r13719 to now in trunk, and
 from r13735 to now in 8.3 (including 8.3pl{1,2,3}) couldn't accurately
 detect universe inconsistencies, leading to potential proofs of False!
 Oups, sorry...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@14996 85f007b7-540e-0410-9357-904b9bb8a0f7
correcting a little bug in invfun.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15006 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: a faster is_leq test used when possible

 Let's reintroduce the idea of stopping the graph traversal as
 soon as a LE arc has been found, but this time we do so only
 when we're not interested by the LT/LE distinction.

 This way, we should remain correct but avoid largly the time penalty
 induced by the last fix on univ.ml: the +30% on contrib Container
 is almost gone, let's hope it'll be the same with Ssreflect.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15014 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: a better Constraint.compare

Let's gain a few % by not using Pervasive.compare on a structure containing
some universe_levels, but rather UniverseLevel.compare on them.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15015 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: a univ_depends function to avoid a hack in Inductiveops

 univ_depends checks whether a universe variable appears or
 is equal to a universe. In comparison with the previous hack
 in inductiveops based on try...catching UniverseInconsistency,
 this should be semantically equivalent, simplier, and more
 robust in case we allow someday an unsafe mode where
 merge_constraints would be a no-op.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15016 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: Erasure of code whose only use were to forbid use of gtk >= 2.24.11 on MacOS

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15024 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: 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/branches/v8.4@15028 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: 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/branches/v8.4@15042 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Removing redundant entry int_nelist and removing extra space when
printing occurrences list.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15045 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: 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/branches/v8.4@15047 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/branches/v8.4@15050 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/branches/v8.4@15051 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 2709: Duplication in coqdoc index entries

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15056 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic
tactic arguments of ltac functions).

Added support for recursive entries in ARGUMENT EXTEND, for right-hand
sides of ARGUMENT EXTEND raising exceptions and for right-hand sides
referring to "loc". Also fixed parsing level of initial value in
create_arg (raw instead of glob). Thanks to the Ssreflect plugin for
revealing these problems.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15066 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing alpha-conversion bug #2723 introduced in r12485-12486.

The optimisation done of Namegen.visibly_occur_id did not preserve
the previous behavior when pr_constr/constr_extern/detype were
called on a term with free rel variables. We backtrack on it to
go back to the 8.2 behavior.

Seized this opportunity to clarify the meaning of the at_top flag
in constrextern.ml and printer.ml and to rename it into
goal_concl_style. The badly-named at_top flag was introduced in
Coq 6.3 in 1999 to mean that when printing variables bound in the
goal, names had to avoid the names of the variables of the goal
context, so as to keep naming stable when using "intro"; in
r4458, printing improved by not avoiding names that were short
names of global definitions, e.g. "S", or "O" (except when the
at_top flag was on for compatibility reasons).

Other printing strategies could be possible in the
non-goal-concl-style mode. For instance, all bound variables
could be made distinct in a given expression, even if no clash
occur, therefore following so-called Barendregt's
convention. This could be done by setting "avoid"
to "ids_of_rel_context (rel_context env)" in extern_constr and
extern_type (and then, Namegen.visibly_occur_id could be
re-simplified again!).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15068 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.3: Fixing alpha-conversion bug #2723 introduced in r12485-12486.

The optimisation done of Namegen.visibly_occur_id did not preserve
the previous behavior when pr_constr/constr_extern/detype were
called on a term with free rel variables. We backtrack on it to
go back to the 8.2 behavior.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15069 85f007b7-540e-0410-9357-904b9bb8a0f7