In :search, check injectivity to prevent erroneous results
Discover typeclass introduction/elimination in :search
Find best matching types first in :search with a priority queue.
Ignore believe_me in :search since its type is a lie!
Merge pull request #1331 from david-christiansen/quasiquote

Quasiquote support
Merge pull request #1341 from bmsherman/improvedSearch

Improve :search results by checking injectivity and allowing typeclass introduction
javascript: optimize constructor allocation
javascript: inline some SLIDEs and PROJECTs
javascript: fix stray semicolon
Merge pull request #1347 from raichoo/javascript

Javascript
Add goal types to quasiquotes.

A quasiquote expression can be given a goal type for the elaborator,
which helps with disambiguation. For instance, `(() : ()) quotes the
unit constructor, while `(() : Type) quotes the unit type.  Both goal
types and quasiquote are typechecked in the global environment.