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 --- pretyping/coercion.ml | 2 +- pretyping/glob_ops.ml | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) (limited to 'pretyping') diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 7b4b2d42f..7be05ea60 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -99,9 +99,9 @@ open Program let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = let src = Loc.tag ?loc (Evar_kinds.QuestionMark { + Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define opaque; Evar_kinds.qm_name=na; - Evar_kinds.qm_record_field=None; }) in let evd, v = Evarutil.new_evar env !evdref ~src c in evdref := evd; diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 9ed0090ed..24eb66682 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -563,9 +563,7 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo GVar id | PatVar Anonymous when not isclosed -> GHole (Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=Define false; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; + Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Define false; },Namegen.IntroAnonymous,None) | _ -> raise Not_found ) x -- cgit v1.2.3