From 1300da19d13f7e46cf3a4b0b3396604ffc44a6d5 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 27 Jun 2018 22:03:25 +0200 Subject: Change QuestionMark for better record field missing error message. While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields. --- engine/evar_kinds.ml | 11 ++++++++++- engine/proofview.ml | 2 +- engine/termops.ml | 2 +- interp/constrintern.ml | 31 +++++++++++++++++++++++++------ plugins/ltac/extratactics.ml4 | 19 +++++++++++++++---- pretyping/cases.ml | 5 ++++- pretyping/coercion.ml | 6 +++++- pretyping/glob_ops.ml | 6 +++++- pretyping/pretyping.ml | 12 ++++++++++-- tactics/hipattern.ml | 6 +++++- test-suite/output/RecordMissingField.out | 4 ++++ test-suite/output/RecordMissingField.v | 8 ++++++++ vernac/comProgramFixpoint.ml | 6 +++++- vernac/himsg.ml | 8 ++++++-- vernac/obligations.ml | 2 +- 15 files changed, 105 insertions(+), 23 deletions(-) create mode 100644 test-suite/output/RecordMissingField.out create mode 100644 test-suite/output/RecordMissingField.v diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml index 12e2fda8e..bedfd0cbb 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -21,12 +21,21 @@ type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t type subevar_kind = Domain | Codomain | Body +(* maybe this should be a Projection.t *) +type record_field = { fieldname : Constant.t; recordname : Names.inductive } + +type question_mark = { + qm_obligation: obligation_definition_status; + qm_name: Name.t; + qm_record_field: record_field option; +} + type t = | ImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t | NamedHole of Id.t (* coming from some ?[id] syntax *) - | QuestionMark of obligation_definition_status * Name.t + | QuestionMark of question_mark | CasesType of bool (* true = a subterm of the type *) | InternalHole | TomatchTypeParameter of inductive * int diff --git a/engine/proofview.ml b/engine/proofview.ml index b4afb6415..12d31e5f4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -754,7 +754,7 @@ let mark_in_evm ~goal evd content = - GoalEvar (morally not dependent) - VarInstance (morally dependent of some name). This is a heuristic for naming these evars. *) - | loc, (Evar_kinds.QuestionMark (_,Names.Name id) | + | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} | Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x | loc,_ -> loc,Evar_kinds.GoalEvar } diff --git a/engine/termops.ml b/engine/termops.ml index 2b179c43b..e4c8ae66b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -114,7 +114,7 @@ let pr_evar_suggested_name evk sigma = | None -> match evi.evar_source with | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id | _,Evar_kinds.VarInstance id -> id - | _,Evar_kinds.QuestionMark (_,Name id) -> id + | _,Evar_kinds.QuestionMark {Evar_kinds.qm_name = Name id} -> id | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" | _ -> let env = reset_with_named_context evi.evar_hyps (Global.env()) in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 18d6c1a5b..f7a1f3bf3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -566,7 +566,11 @@ 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 (st,Anonymous), IntroAnonymous, None)) + DAst.make (GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=st; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, None)) let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous @@ -1370,7 +1374,8 @@ let sort_fields ~complete loc fields completer = (* the order does not matter as we sort them next, List.rev_* is just for efficiency *) let remaining_fields = - let complete_field (idx, _field_ref) = (idx, completer idx) in + let complete_field (idx, field_ref) = (idx, + completer idx field_ref record.Recordops.s_CONST) in List.rev_map complete_field remaining_projs in List.rev_append remaining_fields acc in @@ -1524,7 +1529,7 @@ let drop_notations_pattern looked_for genv = | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id) | CPatRecord l -> let sorted_fields = - sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in + sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in begin match sorted_fields with | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> @@ -1918,8 +1923,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in let fields = sort_fields ~complete:true loc fs - (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)), - IntroAnonymous, None)) + (fun _idx fieldname constructorname -> + let open Evar_kinds in + let fieldinfo : Evar_kinds.record_field = + {fieldname=fieldname; recordname=inductive_of_constructor constructorname} + in + CAst.make ?loc @@ CHole (Some + (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=st; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=Some fieldinfo + }) , IntroAnonymous, None)) in begin match fields with @@ -2002,7 +2016,12 @@ 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 (st,Anonymous)) + | _ -> Evar_kinds.QuestionMark + { + Evar_kinds.qm_obligation=st; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }) | Some k -> k in let solve = match solve with diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f24ab2bdd..dc027c404 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -604,8 +604,11 @@ let subst_var_with_hole occ tid t = else (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), - IntroAnonymous, None))) + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, None))) else x | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t @@ -616,13 +619,21 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec c = match DAst.get c with - | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) -> + | GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s)) + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + },IntroAnonymous,s)) | _ -> map_glob_constr_left_to_right substrec c in substrec t 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) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index f9c4bed35..9d2288346 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -263,7 +263,11 @@ open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) let mkGApp f args = DAst.make @@ GApp (f, args) let mkGHole = DAst.make @@ - GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None) + GHole (QuestionMark { + Evar_kinds.qm_obligation=Define false; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None + }, Namegen.IntroAnonymous, None) let mkGProd id c1 c2 = DAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) let mkGArrow c1 c2 = DAst.make @@ diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out new file mode 100644 index 000000000..7c80a6065 --- /dev/null +++ b/test-suite/output/RecordMissingField.out @@ -0,0 +1,4 @@ +File "stdin", line 8, characters 5-22: +Error: Cannot infer field y2p of record point2d in environment: +p : point2d + diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v new file mode 100644 index 000000000..84f1748fa --- /dev/null +++ b/test-suite/output/RecordMissingField.v @@ -0,0 +1,8 @@ +(** Check for error message when missing a record field. Error message +should contain missing field, and the inferred type of the record **) + +Record point2d := mkPoint { x2p: nat; y2p: nat }. + + +Definition increment_x (p: point2d) : point2d := + {| x2p := x2p p + 1; |}. diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index eef7afbfb..00d14f5b0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -187,7 +187,11 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let sigma, def = let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in let sigma, h_e_term = Evarutil.new_evar env sigma - ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in + ~src:(Loc.tag @@ Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define false; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }) wf_proof in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in let sigma, def = Typing.solve_evars env sigma def in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 534e58f9c..c49ffe267 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -520,11 +520,15 @@ let pr_trailing_ne_context_of env sigma = then str "." else (str " in environment:"++ pr_context_unlimited env sigma) -let rec explain_evar_kind env sigma evk ty = function +let rec explain_evar_kind env sigma evk ty = + let open Evar_kinds in + function | Evar_kinds.NamedHole id -> strbrk "the existential variable named " ++ Id.print id - | Evar_kinds.QuestionMark _ -> + | Evar_kinds.QuestionMark {qm_record_field=None} -> strbrk "this placeholder of type " ++ ty + | Evar_kinds.QuestionMark {qm_record_field=Some {fieldname; recordname}} -> + str "field " ++ (Printer.pr_constant env fieldname) ++ str " of record " ++ (Printer.pr_inductive env recordname) | Evar_kinds.CasesType false -> strbrk "the type of this pattern-matching problem" | Evar_kinds.CasesType true -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1f401b4e1..14d764232 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -220,7 +220,7 @@ let eterm_obligations env name evm fs ?status t ty = in let loc, k = evar_source id evm in let status = match k with - | Evar_kinds.QuestionMark (o,_) -> o + | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o | _ -> match status with | Some o -> o | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ())) -- cgit v1.2.3 From 78321b33b0e5af859f2f57ef96aeb95fad258138 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Sun, 15 Jul 2018 17:40:30 +0200 Subject: Add overlay for Coq-Equations for QuestionMark. The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this. --- ...bollu-questionmark-into-record-for-missing-record-field-error.sh | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh diff --git a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh new file mode 100644 index 000000000..56c0dc343 --- /dev/null +++ b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7941" ] || [ "$CI_BRANCH" = "jun-27-missing-record-field-error-message-quickfix" ]; then + Equations_CI_BRANCH=overlay-question-mark-extended-for-missing-record-field + Equations_CI_GITURL=https://github.com/bollu/Coq-Equations +fi -- cgit v1.2.3 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 --- engine/evar_kinds.ml | 6 ++++++ engine/evar_kinds.mli | 51 ++++++++++++++++++++++++++++++++++++++++++++ interp/constrintern.ml | 18 ++++------------ pretyping/coercion.ml | 2 +- pretyping/glob_ops.ml | 4 +--- tactics/hipattern.ml | 4 +--- vernac/comProgramFixpoint.ml | 4 +--- 7 files changed, 65 insertions(+), 24 deletions(-) create mode 100644 engine/evar_kinds.mli diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml index bedfd0cbb..ea1e57254 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -30,6 +30,12 @@ type question_mark = { qm_record_field: record_field option; } +let default_question_mark = { + qm_obligation=Define true; + qm_name=Anonymous; + qm_record_field=None; +} + type t = | ImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *) diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli new file mode 100644 index 000000000..4facdb200 --- /dev/null +++ b/engine/evar_kinds.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 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 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 diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 9d2288346..7da059ae3 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -264,9 +264,7 @@ let mkPattern c = snd (Patternops.pattern_of_glob_constr c) let mkGApp f args = DAst.make @@ GApp (f, args) let mkGHole = DAst.make @@ GHole (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) let mkGProd id c1 c2 = DAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 00d14f5b0..102a98f04 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -188,9 +188,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in let sigma, h_e_term = Evarutil.new_evar env sigma ~src:(Loc.tag @@ Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=Evar_kinds.Define false; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; + Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false; }) wf_proof in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in -- cgit v1.2.3