diff options
| author | Pierre-Marie Pédrot | 2017-04-07 11:50:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-04-07 11:50:57 +0200 |
| commit | 3a1df73d60372d1966c69450f80a66ca72cb9b44 (patch) | |
| tree | 34f2b0419b52861cb83bb42a90728161c7f792b4 /proofs | |
| parent | d6175b9980808ff91f1299ca26a9a49a117169ca (diff) | |
| parent | 63c73f54023f53a790ef57c9afc22111b9b95412 (diff) | |
Merge branch 'master' into econstr
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 c1a95878f3..7e8ed31d1d 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -234,10 +234,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 Constr.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> @@ -252,3 +252,9 @@ let solve_by_implicit_tactic env sigma evk = sigma, EConstr.of_constr 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 516125ea18..f9fb0b76de 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 * EConstr.constr +val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr) option |