diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-06-05 22:09:15 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-05 22:09:15 +0200 |
commit | 9a618ee0529f7153da1e10a8099a0b691bd13251 (patch) | |
tree | fea027f5f8a97b0f736d553bf4c21a1d62106253 /intf | |
parent | b91f5d1adbd039809e31b5311d06b376829de1fc (diff) | |
parent | ccd8ab4721406991ad63c1e82a880a1f42bf065f (diff) |
Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + a flag suspectingly renamed in a clearer way
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 835e94c77..ac0d96e96 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 33c71884a..5da20c9d1 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -39,7 +39,7 @@ type glob_constr_r = (** An identifier that cannot be regarded as "GRef". Bound variables are typically represented this way. *) | GEvar of existential_name * (Id.t * glob_constr) list - | GPatVar of bool * patvar (** Used for patterns only *) + | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *) | GApp of glob_constr * glob_constr list | GLambda of Name.t * binding_kind * glob_constr * glob_constr | GProd of Name.t * binding_kind * glob_constr * glob_constr |