From b7c7f66f19019fdbf9b9d44e3151c42ce56d5a2f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 28 Sep 2023 15:49:01 +0200 Subject: [PATCH] Ltac2: Avoid generating useless letin when interning `{ foo with ... }` with foo a global name --- plugins/ltac2/tac2intern.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index cc659330e30c..4cb07cb3b644 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -1241,8 +1241,8 @@ let rec intern_rec env tycon {loc;v=e} = in let def = intern_rec_with_constraint env def (GTypRef (Other kn, Array.to_list deftparam)) in let var = match def with - | GTacVar var -> var - | _ -> fresh_var (bound_vars env) + | GTacVar _ | GTacRef _ -> None + | _ -> Some (fresh_var (bound_vars env)) in Some (var, def), args in @@ -1250,14 +1250,15 @@ let rec intern_rec env tycon {loc;v=e} = | PresentField (arg,argty) -> intern_rec_with_constraint env arg argty | MissingField i -> match def with | None -> assert false - | Some (var, _) -> GTacPrj (kn, GTacVar var, i)) + | Some (None, def) -> GTacPrj (kn, def, i) + | Some (Some var, _) -> GTacPrj (kn, GTacVar var, i)) args in let e = GTacCst (Other kn, 0, args) in let e = match def with | None -> e - | Some (var, GTacVar var') when Id.equal var var' -> e - | Some (var, def) -> + | Some (None, _) -> e + | Some (Some var, def) -> GTacLet (false, [Name var, def], e) in check (e, GTypRef (Other kn, tparam))