From 306b45f889f83846b1ab10d3b37d9f3e7817a5db Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Feb 2018 15:30:15 +0100 Subject: Do not compute constr matching context if not used. This mitigates bug #6860. --- plugins/ltac/tactic_matching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index b6462c810..c949589e2 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -46,7 +46,7 @@ let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *) let id_map_try_add id x m = match id with - | Some id -> Id.Map.add id x m + | Some id -> Id.Map.add id (Lazy.force x) m | None -> m (** Adds a binding to a {!Id.Map.t} if the name is [Name id] *) -- cgit v1.2.3