Implement reviewer suggestions

Co-authored-by: jneem <joeneeman@gmail.com>

core/src/error/mod.rs

@@ -1324,12 +1324,8 @@ impl IntoDiagnostics<FileId> for EvalError {
                 );
 
                 vec![Diagnostic::error()
-                    .with_message("non-exhaustive pattern matching")
-                    .with_labels(labels)
-                    .with_notes(vec![
-                        format!("This match expression isn't exhaustive"),
-                        "It has been applied to an argument which doesn't match any of the branches".to_owned(),
-                    ])]
+                    .with_message("unmatched pattern")
+                    .with_labels(labels)]
             }
             EvalError::IllegalPolymorphicTailAccess {
                 action,

core/src/term/pattern/compile.rs

@@ -28,7 +28,7 @@ use crate::{
     term::{make, BinaryOp, MatchData, RecordExtKind, RecordOpKind, RichTerm, Term, UnaryOp},
 };
 
-/// Generate a standard `%record_insert` primop as generated by the parser.
+/// Generate a standard `%record_insert%` primop as generated by the parser.
 fn record_insert() -> BinaryOp {
     BinaryOp::DynExtend {
         ext_kind: RecordExtKind::WithValue,
@@ -393,7 +393,7 @@ impl Compile for MatchData {
     //
     // let value_id = value in
     //
-    // <for (pattern, body) in branches.rev()
+    // <fold (pattern, body) in branches.rev()
     //  - cont is the accumulator
     //  - initial accumulator is the default branch (or error if not default branch)
     // >

core/src/typecheck/operation.rs

@@ -220,7 +220,7 @@ pub fn get_uop_type(
         // Note that is_variant breaks parametricity, so it can't get a polymorphic type.
         // Dyn -> Bool
         UnaryOp::EnumIsVariant() => (mk_uniftype::dynamic(), mk_uniftype::bool()),
-        // [crate::term::UnaryOp::WithEnv] shouldn't appear anywhere in actual code, because its
+        // [crate::term::UnaryOp::PatternBranch] shouldn't appear anywhere in actual code, because its
         // second argument can't be properly typechecked: it has unbound variables. However, it's
         // not hard to come up with a vague working type for it, so we do.
         // forall a. {_ : a} -> Dyn -> Dyn