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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 12 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 |
2 files changed, 10 insertions, 4 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b06ea43bd..9995a9394 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -233,10 +233,10 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac let clear_implicit_tactic () = implicit_tactic := None -let solve_by_implicit_tactic env sigma evk = +let apply_implicit_tactic tac = (); fun env sigma evk -> let evi = Evd.find_undefined sigma evk in - match (!implicit_tactic, snd (evar_source evk sigma)) with - | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) + match snd (evar_source evk sigma) with + | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> @@ -250,3 +250,9 @@ let solve_by_implicit_tactic env sigma evk = sigma, ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit + +let solve_by_implicit_tactic () = match !implicit_tactic with +| None -> None +| Some tac -> Some (apply_implicit_tactic tac) + + diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7458109fa..aad719db4 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr +val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr) option |