diff options
| author | Pierre-Marie Pédrot | 2014-08-23 18:15:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-23 18:31:49 +0200 |
| commit | c2bde259c207f9ff9cb199906879cd1e19a75ced (patch) | |
| tree | c3ef1c619b0411187b1e5c7b03467bfa3b8c10d1 /doc/RecTutorial | |
| parent | 5d3f54fbe38c2f732380140df96e7326c46b7b44 (diff) | |
Tactics.is_quantified_hypothesis does not reduce anymore to decide whether
a variable is quantified in the goal. This is only used by induction, and
it should be a bad practice to depend on an invisible binder.
Diffstat (limited to 'doc/RecTutorial')
0 files changed, 0 insertions, 0 deletions