diff options
| author | Maxime Dénès | 2017-09-26 23:57:40 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-26 23:57:40 +0200 |
| commit | b9740771e8113cb9e607793887be7a12587d0326 (patch) | |
| tree | f69105ad9813738abd10ae824756947940a7dc6d /intf/constrexpr.ml | |
| parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
| parent | 3c964a60d698134c21adc77cbb69ce1528350682 (diff) | |
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Diffstat (limited to 'intf/constrexpr.ml')
| -rw-r--r-- | intf/constrexpr.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 413cd9704b..8eadafe667 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -132,10 +132,6 @@ and constr_notation_substitution = constr_expr list list * (** for recursive notations *) local_binder_expr list list (** for binders subexpressions *) -type typeclass_constraint = (Name.t Loc.located * Id.t Loc.located list option) * binding_kind * constr_expr - -and typeclass_context = typeclass_constraint list - type constr_pattern_expr = constr_expr (** Concrete syntax for modules and module types *) |