* Implementing the "union by rank" optimisation in univ.ml
* Bugfixes in union by rank in univ.ml
* kernel/univ.ml: clarify the rank union selection logic

Author: Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>
Author: Gabriel Scherer <gabriel.scherer@inria.fr>

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16055 85f007b7-540e-0410-9357-904b9bb8a0f7
Coq_makefile: Better rule for subdirs when the subdir does not exist

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16056 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: some more refactoring to lighten coqide.ml

 Main victim is analyzed_view :
  - some unnecessary methods have been killed (hep_for_keyword for instance)
  - some other migrated elsewhere (recenter_input, find_next_occurrence, ...)
  - analyzed_view is now split in two : fileops (filename, save, revert, ...)
    and coqops (process_next_phrase, ...)

 Four new files created:
 - Sentence (for tag_on_insert and alii)
 - FileOps (ex-first-half of analyzed_view)
 - CoqOps (ex-second-half of analyzed_view)
 - Session (ex-record viewable_script and functions about it)

 Also lots of renaming, trying to be shorter (but still meaningful) and
 more uniform

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16057 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: restore the tag removal of copy-pasted zones

 The handler for apply_tag removed in commit 16044 was probaly meant
 for that. We now proceed in a more simple way, in Sentence.split_slice_lax,
 instead of doing a remove_tag in a apply_tag handler (!).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16058 85f007b7-540e-0410-9357-904b9bb8a0f7
Coq_lex: direct accounting of utf8 extra bytes in offsets

 We directly produce in Coq_lex a utf8 char offset instead of
 a byte offset, by counting the utf8 extra byte during the lexing.
 This way, no need anymore for converting later with complex
 byte_offset_to_char_offset.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16059 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: allow editing even during a backtrack

 For that, we removing read-only tags on the backtracked zone
 only at the end of the backtrack

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16060 85f007b7-540e-0410-9357-904b9bb8a0f7
Wg_ScriptView: avoid invalid iters during completion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16061 85f007b7-540e-0410-9357-904b9bb8a0f7
- Fixing parsing so that [Polymorphic] can be applied to gallina extensions.
- When elaborating definitions, make the universes from the type rigid when
checking the term: they should stay abstracted.
- Fix typeclasses eauto's handling of universes for exact hints.
Rework all the code for infering the levels of inductives and checking their
allowed eliminations sorts.

This is based on the computation of a natural level for an inductive type I.
The natural level [nat] of [I : args -> sort := c1 : A1 -> I t1 .. cn : An -> I tn] is
computed by taking the max of the levels of the args (if indices matter) and the
levels of the constructor arguments.
The declared level [decl] of I is [sort], which might be Prop, Set or some Type u (u fresh
or not).
If [decl >= nat && not (decl = Prop && n >= 2)], the level of the inductive is [decl],
otherwise, _smashing_ occured.
If [decl] is impredicative (Prop or Set when Set is impredicative), we accept the
declared level, otherwise it's an error.

To compute the allowed elimination sorts, we have the following situations:
- No smashing occured: all sorts are allowed. (Recall props that are not
smashed are Empty/Unitary props)
- Some smashing occured:
 - if [decl] is Type, we allow all eliminations (above or below [decl],
   not sure why this is justified in general).
 - if [decl] is Set, we used smashing for impredicativity, so only
   small sorts are allowed (Prop, Set).
 - if [decl] is Prop, only logical sorts are allowed: I has either
   large universes inside it or more than 1 constructor.
   This does not treat the case where only a Set appeared in I which
   was previously accepted it seems.

All the standard library works with these changes. Still have to cleanup
kernel/indtypes.ml. It is a good time to have a whiskey with OJ.
Merge branch 'beforepoly' of /Users/mat/research/coq/git into trunk

Fix universe level inference for inductives. Compiles current HoTT/HoTT.
Add [Polymorphic] and [Monomorphic] local flag for definitions as well as
[Set Universe Polymorphism] global flag to make all following definitions
polymorphic. Mainly syntax for now.
First part of the big changes to the kernel:
- Const, Ind, Construct now come with a universe level instance
- It is used for type inference in the kernel, which now also takes
a graph as input: actually a set of local universe variables and their
constraints. Type inference just checks that the constraints are enough
to satisfy its own rules.
- Remove polymorphic_arity and _knowing_parameters everywhere: we
don't need full applications for polymorphism to apply anymore, as
we generate fresh variables at each constant/inductive/constructor
application. However knowing_parameters variants might be reinstated
later for optimization.
- New structures exported in univ.mli:
  - universe_list for universe level instances
  - universe_context(_set) for the local universe constraints, also
recording which variables will be local and hence generalized after
inference if defining a polymorphic ind/constant.
- this patch makes coq stop compiling at indtypes.ml
Adapt kernel, library, pretyping, tactics and toplevel to universe polymorphism.
Various degrees of integration, places where I was not sure what to do or
just postponed bigger reorganizations of the code are marked with FIXMEs.
Main changes:
- Kernel now checks constraints and does not infer them anymore.
- The inference functions produce a context of constraints that were checked
during inference, useful to do double-checking of the univ. poly. code
but might be removed later.
- Constant, Inductive entries now have a universe context (local variables
and constraints) associated to them.
- Printing, debugging functions for the new structures are also implemented.
- Now stopping at Logic.v
- Lots of new code in kernel/univ.ml that should be reviewed.
- kernel/indtypes probably does not do what's right when inferring inductive
type constraints.
- Adapted evd to use the new universe context structure.
- Did not deal with unification/evar_conv.
- Add externalisation code for universe level instances.
- Support for polymorphism in pretyping/command and proofs/proofview etc.
  Needed wrapping of [fresh_.._instance] through the evar_map, which
  contains the local state of universes during type-checking.
- Correct the inductive scheme generation to support polymorphism as well.
- Have to review kernel code for correctness, and especially rework the
  computation of universe constraints for inductives.
Stops somewhat later in Logic.v
- Fix naming of local/toplevel universes to be correctly done at typechecking time:
  local variables have no dirpath.
- Add code to do substitution of universes in modules, not finished yet.
- Move fresh_* functions out of kernel, it won't ever build a universe level again!
- Adapt a lot of new_Type to use the correct dirpath and declare the new types in the evar_map
so we keep track of them.
- A bit of code factorization (evd_comb moved, pretype_global).
- Refactor more code
- Adapt plugins code (sometimes wrong, marked with FIXME)
- Fix cases generating unneeded universe (not sure it's ok though)
- Fix scheme generation for good, might have opportunity to cleanup
the terms later.
Init compiles now (which means rewrite, inversion, elim etc.. work as well).
- Unsolved issue of pretyping to lower sorts properly (to Prop for example).
  This has to do with the (Retyping.get_type_of) giving algebraic universes that
  would appear on the right of constraints.
  This makes checking for dangling universes at the end of pretyping fail,
  hence the check in kernel/univ was removed. It should come back when we have
  a fix for this.
- Correctly (?) compute the levels of inductive types.
  Removed old code pertaining to universe polymorphism. Note that we generate
  constraint variables for the conclusion of inductive types invariably.
- Shrink constraints before going to the kernel, combine substitution of the
  smaller universe set with normalization of evars (maybe not done everywhere,
  only ordinary inductives, definitions and proofs)
- More API reworks overall. tclPUSHCONTEXT can be used to add fresh universes
  to the proof goal (used in a few places to get the right instance.
- Quick fix for auto that won't work in the long run. It should always have been
  restricted to take constant references as input, without any loss of generality
  over constrs.
Fix some plugins and insertion of non-polymorphic constants in a module.
Now stops in relation classes.
Cleanup and move code from kernel to library and from pretyping to library too.
Now there is a unique universe counter declared in library/universes.ml along
with all the functions to generate new universes and get fresh constant/inductive
terms.
- Various function renamings
- One important change in kernel/univ.ml: now [sup] can be applied to Prop.
- Adapt records/classes to universe polymorphism
- Now stops in EqDepFacts due to imprecise universe polymorphism.