diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-10 19:23:58 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-10 19:23:58 +0000 |
| commit | e2655d38d11b072da0e5f4d40b05adbea73c8b8d (patch) | |
| tree | 7fa52c241089222050a84d2b47576e58d6e8492e /library | |
| 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')
| -rw-r--r-- | library/nameops.ml | 2 | ||||
| -rw-r--r-- | library/nameops.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index 6c5000dfe..563fa0210 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 diff --git a/library/nameops.mli b/library/nameops.mli index 336099a2f..10dfecc48 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -34,6 +34,7 @@ val next_name_away_with_default : val out_name : name -> identifier val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a +val name_iter : (identifier -> unit) -> name -> unit val name_cons : name -> identifier list -> identifier list val name_app : (identifier -> identifier) -> name -> name val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * name |