diff options
| author | Maxime Dénès | 2017-04-06 18:02:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-06 18:02:18 +0200 |
| commit | 97b14fa4507d1713213a3dff70a3ddd413cd4d16 (patch) | |
| tree | 77951cd3c8840e01fc85e67010f4abd0925e3cb4 /proofs | |
| parent | 91b82f5a7b3cff65aeadd7c8323d63bf91b5f2e1 (diff) | |
| parent | 8131e35caaacf86cd52262329ab1b0aaa1b8c5b3 (diff) | |
Merge PR#508: Optimize pending evars
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 b06ea43bdd..9995a9394a 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 7458109fa1..aad719db49 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 |