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 993ed300b..5619b7af2 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -601,10 +601,6 @@ val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
(* 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. *)