aboutsummaryrefslogtreecommitdiff
path: root/API/API.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2017-11-30 14:58:45 +0100
committerGaëtan Gilbert2017-11-30 14:58:45 +0100
commit4baccd824d1fe40c57b25c6d3ce04a54c6a38420 (patch)
treefc9a26300e3dc775c86151db3142b23625be8b1c /API/API.mli
parentee45637ac2431fe2df1994f2337d8801e2aeff9a (diff)
Remove unused boolean from cl_context field of Typeclasses.typeclass
Diffstat (limited to 'API/API.mli')
-rw-r--r--API/API.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli
index 1a84600ec9..6c9ac98ffe 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4285,7 +4285,7 @@ sig
type typeclass = {
cl_univs : Univ.AUContext.t;
cl_impl : Globnames.global_reference;
- cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t;
+ cl_context : Globnames.global_reference option list * Context.Rel.t;
cl_props : Context.Rel.t;
cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option
* Names.Constant.t option) list;