Removing useless evar-related stuff.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16803 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 21 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index bfb5ee27c..c8b63ea0f 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -109,27 +109,6 @@ val make_clenv_binding_apply :
 val make_clenv_binding :
   Goal.goal sigma -> constr * constr -> constr bindings -> clausenv
 
-(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
-   [lmetas] is a list of metas to be applied to a proof of [t] so that
-   it produces the unification pattern [ccl]; [sigma'] is [sigma]
-   extended with [lmetas]; if [n] is defined, it limits the size of
-   the list even if [ccl] is still a product; otherwise, it stops when
-   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
-   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
-   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
-   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
-val clenv_environments :
- evar_map -> int option -> types -> evar_map * constr list * types
-
-(** [clenv_environments_evars env sigma n t] does the same but returns
-   a list of Evar's defined in [env] and extends [sigma] accordingly *)
-val clenv_environments_evars :
- env -> evar_map -> int option -> types -> evar_map * constr list * types
-
-(** [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
-val clenv_conv_leq :
- env -> evar_map -> types -> constr -> int -> constr list
-
 (** if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
 val clenv_push_prod : clausenv -> clausenv