From e2655d38d11b072da0e5f4d40b05adbea73c8b8d Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 10 Apr 2009 19:23:58 +0000
Subject: 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
---
 library/nameops.ml  | 2 ++
 library/nameops.mli | 1 +
 2 files changed, 3 insertions(+)

(limited to 'library')

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 
diff --git a/library/nameops.mli b/library/nameops.mli
index 336099a2ff..10dfecc484 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
-- 
cgit v1.2.3