diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:15:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:40:22 +0200 |
| commit | 7943b1fade775af48917d54878e65b80217be038 (patch) | |
| tree | 1ea76a0ca0fb5b9a1c1699842268324cae4c1488 /intf | |
| parent | 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (diff) | |
Using a more explicit algebraic type for evars of kind "MatchingVar".
A priori considered to be a good programming style.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/evar_kinds.mli | 5 | ||||
| -rw-r--r-- | intf/glob_term.mli | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 470ad2a23..75dad2e91 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -8,6 +8,7 @@ open Names open Globnames +open Misctypes (** The kinds of existential variable *) @@ -16,6 +17,8 @@ open Globnames type obligation_definition_status = Define of bool | Expand +type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar + type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) @@ -27,6 +30,6 @@ type t = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase - | MatchingVar of bool * Id.t + | MatchingVar of matching_var_kind | VarInstance of Id.t | SubEvar of Constr.existential_key diff --git a/intf/glob_term.mli b/intf/glob_term.mli index ced5a8b44..ba4a47a36 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -38,7 +38,7 @@ type glob_constr = (** An identifier that cannot be regarded as "GRef". Bound variables are typically represented this way. *) | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list - | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) + | GPatVar of Loc.t * Evar_kinds.matching_var_kind (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr |