From f8c86dca5037d4f79dbb58a41dd3b9f1c5ce8cb5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 24 Oct 2023 17:10:27 +0200 Subject: [PATCH] Tac2intern.intern_let_rec: don't pass unused argument `ids` --- plugins/ltac2/tac2intern.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index 6e3e43639e87..2fbb7c17c4fc 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -1177,7 +1177,7 @@ let rec intern_rec env tycon {loc;v=e} = times in this matching") in let ids = List.fold_left fold Id.Set.empty el in - if is_rec then intern_let_rec env loc ids el tycon e + if is_rec then intern_let_rec env loc el tycon e else intern_let env loc ids el tycon e | CTacSyn (el, kn) -> let body = Tac2env.interp_notation kn in @@ -1338,7 +1338,7 @@ and intern_let env loc ids el tycon e = let (e, t) = intern_rec env tycon e in (GTacLet (false, el, e), t) -and intern_let_rec env loc ids el tycon e = +and intern_let_rec env loc el tycon e = let map env (pat, t, e) = let na = match pat.v with | CPatVar na -> na