aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 9c6cd60bc..9c40c8b71 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -584,10 +584,6 @@ val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -
(* constr with holes and pending resolution of classes, conversion *)
(* problems, candidates, etc. *)
-type pending = (* before: *) evar_map * (* after: *) evar_map
-
-type pending_constr = pending * constr
-
type open_constr = evar_map * constr (* Special case when before is empty *)
(** Partially constructed constrs. *)