Correction d'un bug historique de do_restrict_hyps + code mort

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

1 files changed, 1 insertions, 12 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 763bfa54d9..2de116b612 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -155,16 +155,6 @@ let new_untyped_evar =
   let evar_ctr = ref 0 in
   fun () -> incr evar_ctr; existential_of_int !evar_ctr
 
-let make_evar_instance env =
-  fold_named_context
-    (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*))
-    env ~init:[]
-
-(* create an untyped existential variable *)
-let new_untyped_evar_in_sign env =
-  let ev = new_untyped_evar () in
-  mkEvar (ev, Array.of_list (make_evar_instance env))
-
 (*------------------------------------*
  * functional operations on evar sets *
  *------------------------------------*)
@@ -262,10 +252,9 @@ let do_restrict_hyps evd ev args =
   in
   let sign' = List.rev rsign in
   let env' = reset_with_named_context sign' env in
-  let instance = make_evar_instance env' in
   let (evd',nc) =
     new_evar_instance sign' !evd evi.evar_concl
-      ~src:(evar_source ev !evd) instance in
+      ~src:(evar_source ev !evd) ncargs in
   evd := Evd.evar_define ev nc evd';
   nc