From 83afcfd21be0084b2eff33ffd9e2d8b785679d4a Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Tue, 17 Jul 2018 01:14:36 +0200 Subject: change into QuestionMark default --- interp/constrintern.ml | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f7a1f3bf3..1f37d6367 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -566,11 +566,7 @@ let term_of_name = function | Name id -> DAst.make (GVar id) | Anonymous -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - DAst.make (GHole (Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=st; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; - }, IntroAnonymous, None)) + DAst.make (GHole (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st }, IntroAnonymous, None)) let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous @@ -1929,11 +1925,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = {fieldname=fieldname; recordname=inductive_of_constructor constructorname} in CAst.make ?loc @@ CHole (Some - (Evar_kinds.QuestionMark { + (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st; - Evar_kinds.qm_name=Anonymous; Evar_kinds.qm_record_field=Some fieldinfo - }) , IntroAnonymous, None)) + }) , IntroAnonymous, None)) in begin match fields with @@ -2016,12 +2011,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in (match naming with | IntroIdentifier id -> Evar_kinds.NamedHole id - | _ -> Evar_kinds.QuestionMark - { - Evar_kinds.qm_obligation=st; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; - }) + | _ -> Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st; }) | Some k -> k in let solve = match solve with -- cgit v1.2.3