diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-31 21:31:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 15:06:53 +0200 |
| commit | 2418cf8d5ff6f479a5b43a87c861141bf9067507 (patch) | |
| tree | c9c9f026f3f5f2c2951a668bcf05f909ecfaa80c /pretyping/pretyping.mli | |
| parent | cb0dea2a0c2993d4ca7747afc61fecdbb1c525b1 (diff) | |
Granting Jason's request for an ad hoc compatibility option on
considering trivial unifications "?x = t" in tactics working under
conjunctions (see #3545).
Also updating and fixing wrong comments in test apply.v.
Diffstat (limited to 'pretyping/pretyping.mli')
0 files changed, 0 insertions, 0 deletions