diff options
| author | Matthieu Sozeau | 2015-04-10 18:28:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-04-10 18:28:12 +0200 |
| commit | a86ae4d352cc8e4ac306f04d5536d7fff04d3303 (patch) | |
| tree | bf7aa3e7cdf5be6f68a1c8784ec53ce9d93f1e5c /plugins | |
| parent | 07d63e1333dc73eda3e49e904ff8df6e7f62fa79 (diff) | |
Fix #3590 for good this time, by changing the API, change's argument now
takes a variable substitution for matched variables in the (lhs) pattern, and
uses the existing ist structure to pretype the rhs correcly, without
having to deal with the volatile evars.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b1cbea51c8..86b5e414fe 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -675,7 +675,7 @@ let mkDestructEq : [Simple.generalize new_hyps; (fun g2 -> Proofview.V82.of_tactic (change_in_concl None - (fun sigma -> + (fun patvars sigma -> pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert |