diff options
| author | Matthieu Sozeau | 2016-07-07 10:38:52 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-07 10:54:28 +0200 |
| commit | 2d06b0d8ed38a2c7bc819b418af070cfe865a1d8 (patch) | |
| tree | d9f24bc29c91dbeeb608cf0dc2d191ff2b95290a /interp/constrintern.ml | |
| parent | d0afde58b3320b65fc755cca5600af3b1bc9fa82 (diff) | |
Program: fix #4873: transparency option not used
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1c50253d9c..c0c38a183d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1609,11 +1609,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (merge_impargs l args) loc | CRecord (loc, fs) -> - let fields = - sort_fields ~complete:true loc fs - (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None)) - in - begin + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + let fields = + sort_fields ~complete:true loc fs + (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st), + Misctypes.IntroAnonymous, None)) + in + begin match fields with | None -> user_err_loc (loc, "intern", str"No constructor inference.") | Some (n, constrname, args) -> @@ -1683,7 +1685,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = GIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k, naming, solve) -> let k = match k with - | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true) + | None -> + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + Evar_kinds.QuestionMark st | Some k -> k in let solve = match solve with |