Small cleaning of Evd interface.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16483 85f007b7-540e-0410-9357-904b9bb8a0f7
Moved isolated test params_ind.v to Inductive.v.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16485 85f007b7-540e-0410-9357-904b9bb8a0f7
Share more information between constructors and arity of an inductive
type in order to solve implicit arguments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16486 85f007b7-540e-0410-9357-904b9bb8a0f7
Declaration of multiple hypotheses or parameters now share typing
information for inference of implicit arguments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16487 85f007b7-540e-0410-9357-904b9bb8a0f7
Alert when using ".." outside a Notation command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16488 85f007b7-540e-0410-9357-904b9bb8a0f7
Protection against "Bad recursive type" in w_unify0 (bug #3036).

Morally, unification wants to unify "fun x:Meta => Meta"
with "fun x:nat => match x with ... end". Retyping is asked to
type "match x with ... end" in the context "x:Meta" where the
type of x has de facto been lost. Retyping fails.

I don't see an easy remedy since w_unify0 builds the unifier
lazily, and I'm not sure it is worth to propagate the unifier to
retyping so that it knows it. After all, the call to retyping in
w_unify0 is not so critical.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16489 85f007b7-540e-0410-9357-904b9bb8a0f7
Uniformizing the [if_warn] flag used for warning printing and put
it into the standard logger instead.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
add Loadpath to printers.mllib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16492 85f007b7-540e-0410-9357-904b9bb8a0f7
Xml_datatype.mli ships the xml type

This breaks the dependency of Xml_parser, Xml_printer and Xml_utils
on Serialize.

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

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16495 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing r16487 on sharing evars between multiple parameters (missing List.rev).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16496 85f007b7-540e-0410-9357-904b9bb8a0f7
Uniformization: isevars -> evdref/sigma/evd

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16498 85f007b7-540e-0410-9357-904b9bb8a0f7
A uniformization step around understand_* and interp_* functions.

- Clarification of the existence of three algorithms for solving
  unconstrained evars:
  - the type-class mechanism
  - the heuristics for solving pending conversion problems and multi-candidates
  - Declare Implicit Tactic (when called from tactics)

  Main function for solving unconstrained evars (when not using
  understand): Pretyping.solve_remaining_evars

- Clarification of the existence of three corresponding kinds of
  errors when reporting about unsolved evars:

  Main function for checking resolution of evars independently of the
  understand functions: Pretyping.check_evars_are_solved

- Introduction of inference flags in pretyping for governing which
  combination of the algorithms to use when calling some understand
  function; there is also a flag of expanding or not evars and for
  requiring or not the resolution of all evars

- Less hackish way of managing Pretyping.type_constraint: all three
  different possibilities are now represented by three different
  constructors

- Main semantical changes done:
  - solving unconstrained evars and reporting is not any longer mixed:
    one first tries to find unconstrained evars by any way possible;
    one eventually reports on the existence of unsolved evars using
    check_evars_are_solved
  - checking unsolved evars is now done by looking at the evar map,
    not by looking at the evars occurring in the terms to pretype; the
    only observed consequence so far is in Cases.v because of subterms
    (surprisingly) disappering after compilation of pattern-matching
  - the API changed, see dev/doc/changes.txt

Still to do:

- Find more uniform naming schemes:
  - for distinguishing when sigma is passed as a reference or as a value
    (are used: suffix _evars, prefix e_)
  - for distinguishing when evars are allowed to remain uninstantiated or not
    (are used: suffix _evars, again, suffix _tcc, infix _open_)
  - be more consistent on the use of names evd/sigma/evars or evdref/evars
- By the way, shouldn't "understand" be better renamed into "infer" or
  "preinfer", or "pretype". Grammatically, "understanding a term" looks
  strange.
- Investigate whether the inference flags in tacinterp.ml are really
  what we want (e.g. do we really want that heuristic remains
  activated when typeclasses are explicitly deactivated, idem in
  Tacinterp.interp_open_constr where flags are strange).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7
Getting rid of module Gmapl.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16501 85f007b7-540e-0410-9357-904b9bb8a0f7
Use definition_entry to declare local definitions

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