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 /plugins/ltac/extratactics.ml4 | |
| 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 'plugins/ltac/extratactics.ml4')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 1223f6eb4..7a9fc6657 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -38,7 +38,7 @@ let with_delayed_uconstr ist c tac = let flags = { Pretyping.use_typeclasses = false; solve_unification_constraints = true; - use_hook = Some Pfedit.solve_by_implicit_tactic; + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } in @@ -341,10 +341,10 @@ END (**********************************************************************) (* Refine *) -let constr_flags = { +let constr_flags () = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic; + Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = false; Pretyping.expand_evars = true } @@ -353,7 +353,7 @@ let refine_tac ist simple with_classes c = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = - { constr_flags with Pretyping.use_typeclasses = with_classes } in + { constr_flags () with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in |