diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-23 08:38:00 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-23 11:54:48 +0100 |
commit | f9526a2bcd05174b7adfe56b7375f0306a2a1e6d (patch) | |
tree | 30b53903ae8d1d840090a204211b9ab7895ee879 /tactics | |
parent | 8cfe40dbc02156228a529c01190c50d825495013 (diff) |
Fast path for implicit tactic solving.
We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1e8082f88..8b3442c05 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1146,7 +1146,7 @@ let run_delayed env sigma c = let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = Some solve_by_implicit_tactic; + Pretyping.use_hook = solve_by_implicit_tactic (); Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } |