From de18f227080f375428b29b2fefd612e655ec31bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 24 Oct 2023 17:33:25 +0200 Subject: [PATCH] Tac2intern: use intern_rec_with_constraint more --- plugins/ltac2/tac2intern.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index d5c8f82baca3..f777a9efd40d 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -1156,7 +1156,7 @@ let rec intern_rec env tycon {loc;v=e} = let (f, ft) = intern_rec env None f in let fold t arg = let dom, codom = tycon_app ?loc env ~ft t in - let (arg, argt) = intern_rec env (Some dom) arg in + let arg = intern_rec_with_constraint env arg dom in (codom, arg) in let (t, args) = CList.fold_left_map fold ft args in @@ -1196,7 +1196,7 @@ let rec intern_rec env tycon {loc;v=e} = let e = intern_rec_with_constraint env e (GTypRef (Other t_bool, [])) in let (e1, t1) = intern_rec env tycon e1 in let t = Option.default t1 tycon in - let (e2, t2) = intern_rec env (Some t) e2 in + let e2 = intern_rec_with_constraint env e2 t in (GTacCse (e, Other t_bool, [|e1; e2|], [||]), t) | CTacCse (e, pl) -> let e,brs,rt = intern_case env loc e tycon pl in @@ -1356,7 +1356,7 @@ and intern_let_rec env el tycon e = let (env, el) = List.fold_left_map map env el in let map (na, tc, e) = let loc_e = e.loc in - let (e, t) = intern_rec env (Some tc) e in + let e = intern_rec_with_constraint env e tc in let () = if not (is_rec_rhs e) then user_err ?loc:loc_e (str "This kind of expression is not allowed as \