From f2a46998e4f791309d74445cf43981aedec28fd1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 17 Apr 2009 17:39:40 +0000
Subject: - Fix handling of clauses in setoid_rewrite to rewrite under binders
 correctly. - Fix the new autorewrite to implement the (unstated) invariant
 that the last declared rules are applied first, which makes a difference for
 non-confluent rewrite rules. Some scripts in CoLoR rely on that.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12092 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/term_dnet.ml  | 3 +++
 pretyping/term_dnet.mli | 2 ++
 2 files changed, 5 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 656a90c704..4c6c5e6310 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -367,6 +367,8 @@ struct
     possibly_under app_pat (search_pat pat (pat_of_constr pat)) dn init
 
   let find_all dn = Idset.elements (TDnet.find_all dn)
+
+  let map f dn = TDnet.map f (fun x -> x) dn
 end
     
 module type S =
@@ -385,4 +387,5 @@ sig
   val search_head_concl : t -> constr -> result list
   val search_eq_concl : t -> constr -> constr -> result list
   val find_all : t -> ident list
+  val map : (ident -> ident) -> t -> t
 end
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index ccf9624814..f6c1b5b611 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.mli
@@ -102,6 +102,8 @@ sig
 
   (* [find_all dn] returns all idents contained in dn *)
   val find_all : t -> ident list
+
+  val map : (ident -> ident) -> t -> t
 end
 
 module Make :
-- 
cgit v1.2.3