aboutsummaryrefslogtreecommitdiffhomepage
path: root/API/API.mli
diff options
context:
space:
mode:
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 1a84600ec..6c9ac98ff 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;