From 68fe6e8f354f4317decc5c69e2658fd17b5a5e90 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Nov 2011 23:23:17 +0000
Subject: Finally used typing to decide whether an alias needs to be expanded
 or not in pattern-matching compilation.

Also extended to the Var case the preference given to using the term
to match as alias rather than its expansion.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14737 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 1 +
 lib/util.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index f7be7b0d73..a199aacd23 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -51,6 +51,7 @@ exception Error_in_file of string * (bool * string * loc) * exn
 
 let on_fst f (a,b) = (f a,b)
 let on_snd f (a,b) = (a,f b)
+let map_pair f (a,b) = (f a,f b)
 
 (* Mapping under pairs *)
 
diff --git a/lib/util.mli b/lib/util.mli
index e24df1a315..a2a72453cd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -61,6 +61,7 @@ exception Error_in_file of string * (bool * string * loc) * exn
 
 val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
+val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b
 
 (** Going down pairs *)
 
-- 
cgit v1.2.3