aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 18:01:48 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 18:21:25 +0100
commit3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (patch)
tree45fdbfc2fd03e30105d1ead1e184bdf6ef822de8 /pretyping/pretyping.mli
parentcca57bcd89770e76e1bcc21eb41756dca2c51425 (diff)
parent4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff)
Merge branch 'master'.
Diffstat (limited to 'pretyping/pretyping.mli')
-rw-r--r--pretyping/pretyping.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 47ad93d7e..7284c0655 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -52,7 +52,7 @@ type inference_hook = env -> evar_map -> evar -> evar_map * constr
type inference_flags = {
use_typeclasses : bool;
- use_unif_heuristics : bool;
+ solve_unification_constraints : bool;
use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool