Skip to content

Commit

Permalink
Tac2intern.intern_let_rec: don't pass unused argument loc
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Oct 24, 2023
1 parent f8c86dc commit e0e40c4
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions plugins/ltac2/tac2intern.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 el tycon e
if is_rec then intern_let_rec env el tycon e
else intern_let env loc ids el tycon e
| CTacSyn (el, kn) ->
let body = Tac2env.interp_notation kn in
Expand Down Expand Up @@ -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 el tycon e =
and intern_let_rec env el tycon e =
let map env (pat, t, e) =
let na = match pat.v with
| CPatVar na -> na
Expand All @@ -1350,10 +1350,10 @@ and intern_let_rec env loc el tycon e =
| Some t -> intern_type env t
in
let env = push_name na (monomorphic t) env in
(env, (loc, na, t, e))
(env, (na, t, e))
in
let (env, el) = List.fold_left_map map env el in
let fold (loc, na, tc, e) (el, tl) =
let fold (na, tc, e) (el, tl) =
let loc_e = e.loc in
let (e, t) = intern_rec env (Some tc) e in
let () =
Expand Down

0 comments on commit e0e40c4

Please sign in to comment.