diff options
Diffstat (limited to 'proofs/clenvtac.mli')
| -rw-r--r-- | proofs/clenvtac.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 038f84f01..90d010c80 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -17,12 +17,13 @@ open Evd open Clenv open Proof_type open Tacexpr +open Unification (*i*) (* Tactics *) val unify : constr -> tactic val clenv_refine : evars_flag -> clausenv -> tactic -val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> tactic +val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic (* Compatibility, use res_pf ?with_evars:true instead *) |