diff options
| author | Arnaud Spiwack | 2014-08-01 19:14:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:59 +0200 |
| commit | 94b201b0a7b03978d96b8f8c9d631e4fa4bda4b0 (patch) | |
| tree | 998601ebfb4ad8163bd6c3fb81fabe331c154947 /interp | |
| parent | b240b7d0cfd6233dcb0ba0e3b98354c78c23a0d4 (diff) | |
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.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 |
2 files changed, 3 insertions, 3 deletions
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) |