diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-24 15:58:51 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-24 15:58:51 +0200 |
commit | 0f107c8a747af6bdb40d70d80236f84b325dc35d (patch) | |
tree | 9c0355fb0dba4a48e14d0e5b316c66dfd416d685 /engine | |
parent | 5c34cfa54ec1959758baa3dd283e2e30853380db (diff) | |
parent | 7dfac786626f8f6775dadc0df85360759584c976 (diff) |
Merge PR #6512: [api] Relocate `intf` modules according to dependency-order.
Diffstat (limited to 'engine')
-rw-r--r-- | engine/engine.mllib | 1 | ||||
-rw-r--r-- | engine/evar_kinds.ml | 39 |
2 files changed, 40 insertions, 0 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib index a3614f6c4..a5df5a9fa 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ Universes Univops UState Nameops +Evar_kinds Evd EConstr Namegen diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml new file mode 100644 index 000000000..c964ecf1f --- /dev/null +++ b/engine/evar_kinds.ml @@ -0,0 +1,39 @@ +(************************************************************************) +(* * 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 +open Globnames +open Misctypes + +(** 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 patvar | SecondOrderPatVar of patvar + +type subevar_kind = Domain | Codomain | Body + +type t = + | ImplicitArg of global_reference * (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 + | 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 |