From c397bcc14c2d7ca527f2dd9d5cb8724880e7a2b6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 14 May 2013 18:38:17 +0000
Subject: Mini documentation (evar_absorb_arguments).

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

diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 889b2c9bfd..8e344860f9 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -85,6 +85,10 @@ val define_evar_as_product : evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
 val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
 
+(** Instantiate an evar by as many lambda's as needed so that its arguments
+    are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into
+    [?y[vars1:=args1,vars:=args]] with
+    [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *)
 val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
   evar_map * existential
 
-- 
cgit v1.2.3