aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh6
-rw-r--r--doc/sphinx/language/cic.rst12
-rw-r--r--doc/sphinx/language/coq-library.rst24
-rw-r--r--doc/sphinx/language/gallina-extensions.rst2
-rw-r--r--engine/evar_kinds.ml17
-rw-r--r--engine/evar_kinds.mli51
-rw-r--r--engine/proofview.ml2
-rw-r--r--engine/termops.ml2
-rw-r--r--interp/constrintern.ml21
-rw-r--r--plugins/ltac/extratactics.ml419
-rw-r--r--pretyping/cases.ml5
-rw-r--r--pretyping/coercion.ml6
-rw-r--r--pretyping/glob_ops.ml4
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--tactics/hipattern.ml4
-rw-r--r--test-suite/output/RecordMissingField.out4
-rw-r--r--test-suite/output/RecordMissingField.v8
-rw-r--r--vernac/comProgramFixpoint.ml4
-rw-r--r--vernac/himsg.ml8
-rw-r--r--vernac/obligations.ml2
20 files changed, 175 insertions, 38 deletions
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
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index b01a4ef0f..98e81ebc6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1175,7 +1175,7 @@ ourselves to primitive recursive functions and functionals.
For instance, assuming a parameter :g:`A:Set` exists in the local context,
we want to build a function length of type :g:`list A -> nat` which computes
-the length of the list, so such that :g:`(length (nil A)) = O` and :g:`(length
+the length of the list, such that :g:`(length (nil A)) = O` and :g:`(length
(cons A a l)) = (S (length l))`. We want these equalities to be
recognized implicitly and taken into account in the conversion rule.
@@ -1364,7 +1364,7 @@ irrelevance property which is sometimes a useful axiom:
The elimination of an inductive definition of type :math:`\Prop` on a predicate
:math:`P` of type :math:`I→ Type` leads to a paradox when applied to impredicative
inductive definition like the second-order existential quantifier
-:g:`exProp` defined above, because it give access to the two projections on
+:g:`exProp` defined above, because it gives access to the two projections on
this type.
@@ -1613,7 +1613,7 @@ then the recursive
arguments will correspond to :math:`T_i` in which one of the :math:`I_l` occurs.
The main rules for being structurally smaller are the following.
-Given a variable :math:`y` of type an inductive definition in a declaration
+Given a variable :math:`y` of an inductively defined type in a declaration
:math:`\ind{r}{Γ_I}{Γ_C}` where :math:`Γ_I` is :math:`[I_1 :A_1 ;…;I_k :A_k]`, and :math:`Γ_C` is
:math:`[c_1 :C_1 ;…;c_n :C_n ]`, the terms structurally smaller than :math:`y` are:
@@ -1625,7 +1625,7 @@ Given a variable :math:`y` of type an inductive definition in a declaration
Each :math:`f_i` corresponds to a type of constructor
:math:`C_q ≡ ∀ p_1 :P_1 ,…,∀ p_r :P_r , ∀ y_1 :B_1 , … ∀ y_k :B_k , (I~a_1 … a_k )`
and can consequently be written :math:`λ y_1 :B_1' . … λ y_k :B_k'. g_i`. (:math:`B_i'` is
- obtained from :math:`B_i` by substituting parameters variables) the variables
+ obtained from :math:`B_i` by substituting parameters for variables) the variables
:math:`y_j` occurring in :math:`g_i` corresponding to recursive arguments :math:`B_i` (the
ones in which one of the :math:`I_l` occurs) are structurally smaller than y.
@@ -1801,7 +1801,7 @@ definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`.
.. _The-Calculus-of-Inductive-Construction-with-impredicative-Set:
-The Calculus of Inductive Construction with impredicative Set
+The Calculus of Inductive Constructions with impredicative Set
-----------------------------------------------------------------
|Coq| can be used as a type-checker for the Calculus of Inductive
@@ -1834,7 +1834,7 @@ inductive definitions* like the example of second-order existential
quantifier (:g:`exSet`).
There should be restrictions on the eliminations which can be
-performed on such definitions. The eliminations rules in the
+performed on such definitions. The elimination rules in the
impredicative system for sort :math:`\Set` become:
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index f23e04c3a..52c56d2bd 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -705,21 +705,29 @@ fixpoint equation can be proved.
Accessing the Type level
~~~~~~~~~~~~~~~~~~~~~~~~
-The basic library includes the definitions of the counterparts of some data-types and logical
-quantifiers at the ``Type``: level: negation, pair, and properties
-of ``identity``. This is the module ``Logic_Type.v``.
+The standard library includes ``Type`` level definitions of counterparts of some
+logic concepts and basic lemmas about them.
+
+The module ``Datatypes`` defines ``identity``, which is the ``Type`` level counterpart
+of equality:
+
+.. index::
+ single: identity (term)
+
+.. coqtop:: in
+
+ Inductive identity (A:Type) (a:A) : A -> Type :=
+ identity_refl : identity a a.
+
+Some properties of ``identity`` are proved in the module ``Logic_Type``, which also
+provides the definition of ``Type`` level negation:
.. index::
single: notT (term)
- single: prodT (term)
- single: pairT (term)
.. coqtop:: in
Definition notT (A:Type) := A -> False.
- Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
-
-At the end, it defines data-types at the ``Type`` level.
Tactics
~~~~~~~
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 509ac92f8..d9b249045 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1079,7 +1079,7 @@ The definition of ``N`` using the module type expression ``SIG`` with
Module N : SIG' := M.
-If we just want to be sure that the our implementation satisfies a
+If we just want to be sure that our implementation satisfies a
given module type without restricting the interface, we can use a
transparent constraint
diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 12e2fda8e..ea1e57254 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -21,12 +21,27 @@ 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;
+}
+
+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 *)
| 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/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 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+(** The kinds of existential variable *)
+
+(** Should the obligation be defined (opaque or transparent (default)) or
+ defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
+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 *)
+(* Represents missing record field *)
+type record_field = { fieldname : Constant.t; recordname : Names.inductive }
+
+type question_mark = {
+ qm_obligation: obligation_definition_status;
+ qm_name: Name.t;
+ (* Tracks if the evar represents a missing record field *)
+ qm_record_field: record_field option;
+}
+
+(* Default value of question_mark which is used most often *)
+val default_question_mark : question_mark
+
+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 question_mark
+ | CasesType of bool (* true = a subterm of the type *)
+ | InternalHole
+ | TomatchTypeParameter of inductive * int
+ | GoalEvar
+ | ImpossibleCase
+ | MatchingVar of matching_var_kind
+ | VarInstance of Id.t
+ | SubEvar of subevar_kind option * Evar.t
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 9a4f2177f..cb50245d5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -566,7 +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 (st,Anonymous), 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
@@ -1370,7 +1370,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 +1525,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 +1919,16 @@ 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.default_question_mark with
+ Evar_kinds.qm_obligation=st;
+ Evar_kinds.qm_record_field=Some fieldinfo
+ }) , IntroAnonymous, None))
in
begin
match fields with
@@ -2002,7 +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 (st,Anonymous))
+ | _ -> 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/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..7be05ea60 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.default_question_mark with
+ Evar_kinds.qm_obligation=Evar_kinds.Define opaque;
+ Evar_kinds.qm_name=na;
+ }) 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..24eb66682 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -562,7 +562,9 @@ 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.default_question_mark with Evar_kinds.qm_obligation=Define false;
+ },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..7da059ae3 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -263,7 +263,9 @@ 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.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)
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..102a98f04 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -187,7 +187,9 @@ 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.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
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 ()))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 14:29:40 +0000