diff options
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index fde5a11f15..259690aa97 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1551,8 +1551,10 @@ let internalize globalenv env allow_patvar lvar c = let solve = match solve with | None -> None | Some gen -> - let (cvars, lvars) = fst lvar in + let ((cvars, lvars), ntnvars) = lvar in + let ntnvars = Id.Map.domain ntnvars in let lvars = Id.Set.union lvars cvars in + let lvars = Id.Set.union lvars ntnvars in let ist = { Genintern.ltacvars = lvars; ltacrecvars = Id.Map.empty; |