diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-01 12:48:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-01 13:57:26 +0200 |
| commit | dae240f31d6de1d5b3737d6d0779e009f3d67fa2 (patch) | |
| tree | b3d0aa053c80da8a21fd995b73fcf01d7739707c /proofs/pfedit.ml | |
| parent | d24997ae295ac4bc80b77273e5499b472f193939 (diff) | |
Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).
But there are still bugs with Declare Implicit Tactic, which should
probably rather be reimplemented with ltac:(tac).
Indeed, it does support evars in the type of the term, and
solve_by_implicit_tactic should transfer universe constraints to the
main goal. E.g., the following still fails, at Qed time.
Definition Foo {T}{a : T} : T := a.
Declare Implicit Tactic eassumption.
Goal forall A (x : A), A.
intros.
apply Foo.
Qed.
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a515c9e75..20cae84a4 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -230,8 +230,10 @@ let solve_by_implicit_tactic env sigma evk = (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try + let c = Evarutil.nf_evars_universes sigma evi.evar_concl in + if Evarutil.has_undefined_evars sigma c then raise Exit; let (ans, _, _) = - build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in + build_by_tactic env (Evd.evar_universe_context sigma) c tac in ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit |