chore: rename confusing field name ParamInfo.prop ==> ParamInfo.proof

The type of the parameter is a proposition, but the parameter itself
is a proof.

src/Init/Lean/Meta/Basic.lean

@@ -82,7 +82,7 @@ structure Config :=
 structure ParamInfo :=
 (implicit     : Bool      := false)
 (instImplicit : Bool      := false)
-(prop         : Bool      := false)
+(proof        : Bool      := false)
 (hasFwdDeps   : Bool      := false)
 (backDeps     : Array Nat := #[])
 

src/Init/Lean/Meta/DiscrTree.lean

@@ -133,7 +133,7 @@ private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Arr
 | i, Expr.app f a _, todo =>
   if h : i < infos.size then
     let info := infos.get ⟨i, h⟩;
-    if info.implicit || info.instImplicit || info.prop then
+    if info.implicit || info.instImplicit || info.proof then
       pushArgsAux (i-1) f (todo.push tmpStar)
     else
       pushArgsAux (i-1) f (todo.push a)

src/Init/Lean/Meta/FunInfo.lean

@@ -62,12 +62,12 @@ checkFunInfoCache fn maxArgs? $ do
         (fun (i : Nat) (pinfo : Array ParamInfo) => do
           let fvar := fvars.get! i;
           decl ← getFVarLocalDecl fvar;
-          prop ← isProp decl.type;
+          proof ← isProp decl.type;
           let backDeps := collectDeps fvars decl.type;
           let pinfo    := updateHasFwdDeps pinfo backDeps;
           pure $ pinfo.push {
             backDeps     := backDeps,
-            prop         := prop,
+            proof        := proof,
             implicit     := decl.binderInfo == BinderInfo.implicit,
             instImplicit := decl.binderInfo == BinderInfo.instImplicit })
         #[];