From 5f28b993aaf104f646452f9a83ef763bcb3fa5f3 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 25 Sep 2013 17:53:07 +0000 Subject: Removing useless evar-related stuff. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16803 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/clenv.mli | 21 --------------------- 1 file changed, 21 deletions(-) (limited to 'proofs/clenv.mli') 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 -- cgit v1.2.3