Removing useless evar-related stuff.

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

2 files changed, 10 insertions, 49 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index bc6da8c347..b75c675297 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -83,6 +83,16 @@ let clenv_push_prod cl =
 (* Instantiate the first [bound] products of [t] with metas (all products if
    [bound] is [None]; unfold local defs *)
 
+(** [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] *)
+
 let clenv_environments evd bound t =
   let rec clrec (e,metas) n t =
     match n, kind_of_term t with
@@ -100,34 +110,6 @@ let clenv_environments evd bound t =
   in
   clrec (evd,[]) bound t
 
-(* Instantiate the first [bound] products of [t] with evars (all products if
-   [bound] is [None]; unfold local defs *)
-
-let clenv_environments_evars env evd bound t =
-  let rec clrec (e,ts) n t =
-    match n, kind_of_term t with
-      | (Some 0, _) -> (e, List.rev ts, t)
-      | (n, Cast (t,_,_)) -> clrec (e,ts) n t
-      | (n, Prod (na,t1,t2)) ->
-          let e',constr = Evarutil.new_evar e env t1 in
-	  let dep = dependent (mkRel 1) t2 in
-	  clrec (e', constr::ts) (Option.map ((+) (-1)) n)
-	    (if dep then (subst1 constr t2) else t2)
-      | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
-      | (n, _) -> (e, List.rev ts, t)
-  in
-  clrec (evd,[]) bound t
-
-let clenv_conv_leq env sigma t c bound =
-  let ty = Retyping.get_type_of env sigma c in
-  let evd = Evd.create_goal_evar_defs sigma in
-  let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
-  let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
-  let evars = Evarconv.consider_remaining_unif_problems env evars in
-  let args = List.map (whd_evar evars) args in
-  check_evars env sigma evars (applist (c,args));
-  args
-
 let mk_clenv_from_env environ sigma n (c,cty) =
   let evd = create_goal_evar_defs sigma in
   let (evd,args,concl) = clenv_environments evd n cty in
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index bfb5ee27ca..c8b63ea0fd 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