From ee7f5486fff86c453767997f97eda381983c4bbc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 21 Feb 2018 15:47:51 +0100
Subject: Option for messing with inference of irrelevant constraints

---
 engine/eConstr.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 28c9dd3c2..87531e116 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -196,6 +196,8 @@ 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
-- 
cgit v1.2.3