diff options
Diffstat (limited to 'interp/constrintern.ml')
| -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 bac97aa3f..7eeb81050 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1739,7 +1739,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let k = match k with | None -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - Evar_kinds.QuestionMark st + (match naming with + | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id + | _ -> Evar_kinds.QuestionMark st) | Some k -> k in let solve = match solve with |