From 9b4927d7fdbbafa7ed372e152e7106b3055dfb99 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Jul 2010 21:06:06 +0000
Subject: Constrintern: unified push_name_env and push_loc_name_env; made
 location dumping for binders uniformly treated in constrintern.ml (and
 renamed the optional arg of interp_context from fail_anonymous to
 global_level since the flag now also decides whether to dump binders as
 global or local ones); added locations for the variables occurring in the "as
 in" clauses;

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

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index 20481adf3a..16e00a0899 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -42,6 +42,7 @@ let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
 
 let located_fold_left f x (_,a) = f x a
 let located_iter2 f (_,a) (_,b) = f a b
+let down_located f (_,a) = f a
 
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
@@ -65,6 +66,11 @@ let pi1 (a,_,_) = a
 let pi2 (_,a,_) = a
 let pi3 (_,_,a) = a
 
+(* Projection operator *)
+
+let down_fst f x = f (fst x)
+let down_snd f x = f (snd x)
+
 (* Characters *)
 
 let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
diff --git a/lib/util.mli b/lib/util.mli
index bbef3462ad..e5b6cd5442 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -51,6 +51,7 @@ val user_err_loc : loc * string * std_ppcmds -> 'a
 val invalid_arg_loc : loc * string -> 'a
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
 val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
+val down_located : ('a -> 'b) -> 'a located -> 'b
 
 (** Like [Exc_located], but specifies the outermost file read, the
    input buffer associated to the location of the error (or the module name
@@ -63,6 +64,11 @@ 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
 
+(** Going down pairs *)
+
+val down_fst : ('a -> 'b) -> 'a * 'c -> 'b
+val down_snd : ('a -> 'b) -> 'c * 'a -> 'b
+
 (** Mapping under triple *)
 
 val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
-- 
cgit v1.2.3