diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-05-15 15:13:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-05-15 15:13:49 +0200 |
| commit | 927b3826e645d428ebe3d8c6599c1f9e2bf79d46 (patch) | |
| tree | aa664725086b1e9672ecba6620d940ef34619dcc /plugins/ltac | |
| parent | cfed57b021b89018d1bb30c6aa0957299fe35d8d (diff) | |
| parent | 357c94b3e42d4422e311799771f9e28249fc3608 (diff) | |
Merge PR #7213: Do not compute constr matching context if not used.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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] *) |