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 | |
| 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.
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5c76ce776b..83e282a303 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -677,7 +677,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl = with Redelimination -> None let is_quantified_hypothesis id g = - match pf_lookup_hypothesis_as_renamed_gen true (NamedHyp id) g with + match pf_lookup_hypothesis_as_renamed_gen false (NamedHyp id) g with | Some _ -> true | None -> false |