Complying an ocaml warning.
Fixing #3282 (two bugs in the presence of let-in's in "fix").
Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).
Thanks to David M. Cooke on coq-bugs for pointing out one part
of the problem.
Tentative optimization not to nf_evar too often in the compatibility
layer. To this intent, we add a cache evar_map in goals that is the
latest known one where the goal is nf-evarized. If the current one
and the cache coincide, we leave the goal as-is.
Adapt coercion code to work with projections as target classes.
HoTT coq bug #82 already fixed.
Fix HoTT bug #84, binding scopes to projections.
Continue fix on argument scopes of primitive projections.
Not considering test-suite file #89 as a bug anymore.
Explicit universes allow to write liftings explicitely. Implicit lifting would change the
theory non-trivially.
Bug closed, now in polymorphic mode, Variables A B : Type give different levels to A and B.
Not a bug, keep for backwards compatibility
Reinstate eta for records in evarconv, fixing two HoTT coq bugs.
Fix a destArity that does not exactly match isArity in presence of let-ins.
Dummy commit to test the new setup of coq-commits mailinglist
Dummy commit to test the new setup of coq-commits mailinglist (bis)
Code factorization in LMap.
Proofs now take and return an evar_universe_context, simplifying interfaces
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
Support dropping files over the coqide window. (Partial fix for bug #2765)

The fix is only partial, because dropping files only works over the menu
bar, the icon bar, the status bar, and so on. Editable boxes, such as the
script widget, catch dnd events, hence preventing this code from working
for these drop targets. Some (labl)gtk expert should be able to sort it
out.