aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.mli')
-rw-r--r--engine/eConstr.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 87531e116..28c9dd3c2 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -196,8 +196,6 @@ val whd_evar : Evd.evar_map -> constr -> constr
(** {6 Equality} *)
-val cumul_weak_constraints : bool ref
-
val eq_constr : Evd.evar_map -> t -> t -> bool
val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option