aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evar_kinds.ml6
-rw-r--r--engine/evar_kinds.mli51
-rw-r--r--interp/constrintern.ml18
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/glob_ops.ml4
-rw-r--r--tactics/hipattern.ml4
-rw-r--r--vernac/comProgramFixpoint.ml4
7 files changed, 65 insertions, 24 deletions
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 *)
+(* <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/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
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 22:15:56 +0000