diff options
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) |