From c8a051cc9d85ef425b780a8454e8567e423171b4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 12 Mar 2021 19:20:46 +0100
Subject: Use the new API to prevent retyping of Ltac2 variable quotations.

Fixes #12785: Ltac2 Performance Overhead.
---
 user-contrib/Ltac2/tac2core.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 4f1cee4211..c6c8aef291 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1409,13 +1409,14 @@ let () =
     let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
     let c = Id.Map.find id ist.env_ist in
     let c = Value.to_constr c in
-    let sigma, concl = match tycon with
-    | Some ty -> sigma, ty
-    | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
-    in
-    let sigma = Typing.check (GlobEnv.renamed_env env) sigma c concl in
-    let j = { Environ.uj_val = c; Environ.uj_type = concl } in
-    (j, sigma)
+    let t = Retyping.get_type_of (GlobEnv.renamed_env env) sigma c in
+    match tycon with
+    | None ->
+      { Environ.uj_val = c; Environ.uj_type = t }, sigma
+    | Some ty ->
+      let sigma = Evarconv.unify_leq_delay (GlobEnv.renamed_env env) sigma t ty in
+      let j = { Environ.uj_val = c; Environ.uj_type = ty } in
+      j, sigma
   in
   GlobEnv.register_constr_interp0 wit_ltac2_quotation interp
 
-- 
cgit v1.2.3