From b61d0df2899f5de9c20ee4a2c4b79deb0714b162 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Apr 2007 09:34:32 +0000
Subject: Ajout de la possibilité d'utiliser les evars dans apply_in et
 elim_in. Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
 "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522).

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

(limited to 'pretyping')

diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index b855ee7e0a..944d7d4b39 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -81,6 +81,8 @@ val clenv_unique_resolver :
 val evar_clenv_unique_resolver :
   clausenv -> evar_info sigma -> clausenv
 
+val clenv_pose_dependent_evars : clausenv -> clausenv
+
 (***************************************************************)
 (* Bindings *)
 
-- 
cgit v1.2.3