Small lemma about Relations.
Collecting in Namegen those conventional default names that are used in different places
Make standard library independent of the names generated by
induction/elim over a dependent elimination principle for Prop
arguments.
Make standard library independent of the names generated by
induction/elim over a dependent elimination principle for Prop
arguments.
Removing dead code from Univ.
Dedicated map module for type universes. It uses hashmaps, which are
slightly more efficient than plain balanced maps.
Moving the [split] tactic out of the AST.
Make kernel reduction code parametric over the handling of universes,
allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
Remove the syntax [Vernac1. Vernac2. … Vernacn. ].

It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being.

The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ].

I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr.
Fixes the lost evars when interpreting a change with pattern tactic.
Dead code.
Preserve compatibility on examples such as "intros []." on goals such
as "forall x:nat*nat, x=x", which resulted in
"forall n n0 : nat, (n, n0) = (n, n0)" before commit
37f68259ab0a33c3b5b41de70b08422d9bcd3bec on "Fixing introduction
patterns * and ** ".
Adding a new Control file centralizing the control options of Coq.
Moving a Thread.yield in check_interrupt.
Removing 'open Univ' from checker.
Function in Univ uselessly exported.