From 94b201b0a7b03978d96b8f8c9d631e4fa4bda4b0 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 1 Aug 2014 19:14:27 +0200
Subject: Faster uconstr.

Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.---
 interp/constrintern.ml  | 4 ++--
 interp/constrintern.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 95d902fd40..04e9fceff6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -654,7 +654,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
     GVar (loc,id), [], [], []
   (* Is [id] bound to a glob_constr in the the ltac context *)
   else if Id.Map.mem id ltacsubst then
-    Id.Map.find id ltacsubst, [], [], []
+    Lazy.force (Id.Map.find id ltacsubst), [], [], []
   (* Is [id] a notation variable *)
   else if Id.Map.mem id ntnvars
   then
@@ -1769,7 +1769,7 @@ let scope_of_type_kind = function
   | OfType typ -> compute_type_scope typ
   | WithoutTypeConstraint -> None
 
-type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t
+type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t
 
 let empty_ltac_sign = (Id.Set.empty, Id.Set.empty, Id.Map.empty)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2b61c51dc9..46697253bd 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -67,7 +67,7 @@ val compute_internalization_env : env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t
+type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t
 
 type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
-- 
cgit v1.2.3