From 6afce6741c5436307116559820de96c672b4c501 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 28 Jul 2017 14:10:02 +0200
Subject: refine: obey the use_unification_heuristics flag

---
 proofs/pfedit.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'proofs')

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7b79732249..e02b5ab956 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -85,6 +85,9 @@ val solve : ?with_end_tac:unit Proofview.tactic ->
 
 val by : unit Proofview.tactic -> bool
 
+(** Option telling if unification heuristics should be used. *)
+val use_unification_heuristics : unit -> bool
+
 (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
    existential variable of the current focused proof by [c] or raises a
    UserError if no proof is focused or if there is no such [n]th
-- 
cgit v1.2.3