Added support for several impossible cases in compilation of "match".
English typo in a function name of evarconv.
Moving function about locs in locusops.
Naming main goal "Main"
Adding printers for ppproofview.
Adding a tactic which fails if one of the goals under focus is dependent in another one.
Add support for deactivating type class inference from induction/destruct.