Quelques modifications autour du filtrage Ltac:

- Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas
  où c'est le n-ième sous-termes qui finalement réussit (passage à une
  complexité en n plutôt que n^2, via l'utilisation de continuations).
- Sémantique du filtrage: suppression dans sub_match de la recherche
  dans le type des let (puisque ce n'est pas cencé être une
  information utilisateur) mais rajout de la recherche dans le champ
  cast qui lui est utilisateur.
- Nouvelle fonctionnalité: récupération des noms des variables liantes
  filtrées (dans matches/sub_match) et utilisation de ces noms dans
  ltac (utile pour récupérer x dans "exists x, P x");



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11226 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 5 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index ebade654ef..2a60ad7b02 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -626,6 +626,10 @@ let rec list_remove_first a = function
   | b::l -> b::list_remove_first a l
   | [] -> raise Not_found
 
+let rec list_remove_assoc_in_triple x = function
+  | [] -> []
+  | (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l
+
 let list_add_set x l = if List.mem x l then l else x::l
 
 let list_eq_set l1 l2 =
diff --git a/lib/util.mli b/lib/util.mli
index 7e351e2705..a341fa5a29 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -137,6 +137,7 @@ val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
 val list_remove : 'a -> 'a list -> 'a list
 val list_remove_first : 'a -> 'a list -> 'a list
+val list_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
 val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b