From b1ef8344b53977661e0d58f01f25603d32dfeba2 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 30 May 2013 12:52:43 +0000
Subject: export Unification.abstract_list_all_with_dependencies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16545 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index d667ed9a4a..6fbbc2c5f4 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -55,11 +55,13 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
 
 (*i This should be in another module i*)
 
-(** [abstract_list_all env evd t c l]                       
-   abstracts the terms in l over c to get a term of type t 
+(** [abstract_list_all env evd t c l]
+   abstracts the terms in l over c to get a term of type t
    (exported for inv.ml) *)
 val abstract_list_all :
   env -> evar_map -> constr -> constr -> constr list -> constr * types
+val abstract_list_all_with_dependencies :
+  env -> evar_map -> types -> constr -> constr list -> constr
 
 
 (* For tracing *)
-- 
cgit v1.2.3