diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evar_kinds.ml | 17 | ||||
| -rw-r--r-- | engine/evar_kinds.mli | 51 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 2 |
4 files changed, 69 insertions, 3 deletions
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 |