- 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

1 files changed, 2 insertions, 0 deletions

diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index ccf962481..f6c1b5b61 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 :