Add Ord instance for Bool
Add parens on generated S patterns

This fixes an issue where generated S patterns would sometimes not be
parenthesized, leading to invalid patterns being generated. This
occurred even in tutorial code, like Parity.
Don't do trace when `with` doesn't match

This breaks IDESlave support. RE #879
Merge pull request #1379 from david-christiansen/paren-S-pat

Add parens on generated S patterns
Merge pull request #1377 from puffnfresh/missing-instances

Add Ord instance for Bool
Merge pull request #1380 from david-christiansen/no-trace-on-with

Get rid of `trace` in error def
Remove dodgy unification hack

Also need to recheck unification problems immediately after setting
injective arguments, or we get strange results for disambiguation.
Fixes #1372
Fix scope/matching issues in proof scripts

Need to treat appeals to tactics as independent calls to the elaborator,
with known current scope, so don't add implicits until just before
invoking the tactic, and add a final unify/match step to collect any
missing implicits.
Recheck quasiquotes

This makes the elaborator for quasiquotes somewhat more strict, which
prevents unknown names from sneaking in to quasiquotes as well as
causing it to fail if not enough information is provided to solve implicits.
Update tests for rechecking of quasiquotes
Remove unused code
Generate legal names for infix op lemmas

Fixes #1337
Merge pull request #1382 from david-christiansen/incomplete-quasiquote

Properly type check quasiquotes
Merge pull request #1383 from david-christiansen/issue/1337

Generate legal names for infix op lemmas
javascript: switch to Data.Text for code generation
Merge pull request #1385 from raichoo/javascript

javascript: switch to Data.Text for code generation
javascript: factor AST into own module
javascript: whitespace
javascript: wrap exceptions in function
Merge pull request #1387 from raichoo/javascript

Javascript