diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 5 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 6 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 12 |
4 files changed, 24 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 2d72b9db6..6a63fb02f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2104,7 +2104,10 @@ let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] let hole na = DAst.make @@ - GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation= Evar_kinds.Define false; + Evar_kinds.qm_name=na; + Evar_kinds.qm_record_field=None}, IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5c4cbefad..7b4b2d42f 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -98,7 +98,11 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 = 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.Define opaque,na)) in + let src = Loc.tag ?loc (Evar_kinds.QuestionMark { + 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; v diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 4dfa789ba..9ed0090ed 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -562,7 +562,11 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo | PatVar (Name id) when not isclosed -> GVar id | PatVar Anonymous when not isclosed -> - GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None) + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Define false; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + },Namegen.IntroAnonymous,None) | _ -> raise Not_found ) x diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 57c4d363b..122979c1a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -381,8 +381,16 @@ let adjust_evar_source evdref na c = | Name id, Evar (evk,args) -> let evi = Evd.find !evdref evk in begin match evi.evar_source with - | loc, Evar_kinds.QuestionMark (b,Anonymous) -> - let src = (loc,Evar_kinds.QuestionMark (b,na)) in + | loc, Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=b; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=recfieldname; + } -> + let src = (loc,Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=b; + Evar_kinds.qm_name=na; + Evar_kinds.qm_record_field=recfieldname; + }) in let (evd, evk') = restrict_evar !evdref evk (evar_filter evi) ~src None in evdref := evd; mkEvar (evk',args) |