From caf18e2f8ef3b63337712ba97b0b049184ae9437 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 16 Jul 2008 14:27:10 +0000
Subject: 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
---
 lib/util.ml  | 4 ++++
 lib/util.mli | 1 +
 2 files changed, 5 insertions(+)

(limited to 'lib')

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
-- 
cgit v1.2.3