aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.ml')
-rw-r--r--kernel/term.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index b86ac850c..8bd079ce5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -748,7 +748,7 @@ let substl laml =
substn_many (Array.map make_substituend (Array.of_list laml)) 0
let subst1 lam = substl [lam]
-let substl_decl laml (id,bodyopt,typ as d) =
+let substl_decl laml (id,bodyopt,typ) =
match bodyopt with
| None -> (id,None,substl laml typ)
| Some body -> (id, Some (substl laml body), type_app (substl laml) typ)