diff options
| author | msozeau | 2009-04-10 19:23:58 +0000 |
|---|---|---|
| committer | msozeau | 2009-04-10 19:23:58 +0000 |
| commit | e2655d38d11b072da0e5f4d40b05adbea73c8b8d (patch) | |
| tree | 7fa52c241089222050a84d2b47576e58d6e8492e /library/nameops.ml | |
| parent | 4cc6bd53bca5441c9960ba55818b5ddfa8c8d13b (diff) | |
Fix premature optimisation in dependent induction: even variable args need
to be generalized as they may appear in other arguments or their types.
Try to keep the original names around as well, using the ones found in
the goal. This only requires that interning a pattern [forall x, _]
properly declares [x] as a metavariable, binding instances are already
part of the substitutions computed by [extended_matches].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nameops.ml')
| -rw-r--r-- | library/nameops.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index 6c5000dfef..563fa02102 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -143,6 +143,8 @@ let name_fold f na a = | Name id -> f id a | Anonymous -> a +let name_iter f na = name_fold (fun x () -> f x) na () + let name_cons na l = match na with | Anonymous -> l |