diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 66c453403c..c811a5bc33 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/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 := #[])
 
diff --git a/src/Init/Lean/Meta/DiscrTree.lean b/src/Init/Lean/Meta/DiscrTree.lean
index fbd29d98eb..d6d230697c 100644
--- a/src/Init/Lean/Meta/DiscrTree.lean
+++ b/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)
diff --git a/src/Init/Lean/Meta/FunInfo.lean b/src/Init/Lean/Meta/FunInfo.lean
index 56bc2c9099..ae297a6d6e 100644
--- a/src/Init/Lean/Meta/FunInfo.lean
+++ b/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 })
         #[];