diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:14:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:14:09 +0200 |
| commit | 4f742e14441581ece247d33020055f15732f126b (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /intf | |
| parent | 7943b1fade775af48917d54878e65b80217be038 (diff) | |
Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/evar_kinds.mli | 5 | ||||
| -rw-r--r-- | intf/glob_term.mli | 2 |
2 files changed, 2 insertions, 5 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 75dad2e91..470ad2a23 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -8,7 +8,6 @@ open Names open Globnames -open Misctypes (** The kinds of existential variable *) @@ -17,8 +16,6 @@ open Misctypes 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 *) @@ -30,6 +27,6 @@ type t = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase - | MatchingVar of matching_var_kind + | MatchingVar of bool * Id.t | VarInstance of Id.t | SubEvar of Constr.existential_key diff --git a/intf/glob_term.mli b/intf/glob_term.mli index ba4a47a36..ced5a8b44 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 * Evar_kinds.matching_var_kind (** Used for patterns only *) + | GPatVar of Loc.t * (bool * patvar) (** 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 |