Clear ne substitue plus le corps dans le reste du but

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

1 files changed, 7 insertions, 11 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index ec998ba83d..df6d667722 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -87,23 +87,19 @@ let check_clear_forward cleared_ids used_ids whatfor =
    forces the user to give them in order). *)
 let clear_hyps ids gl =
   let env = Global.env() in
-  let (nhyps,subst,rmv) =
+  let (nhyps,rmv) =
     Sign.fold_named_context
-      (fun (id,c,ty as d) (hyps,subst,rmv) ->
+      (fun (id,c,ty as d) (hyps,rmv) ->
         if List.mem id ids then
-          match c with
-            | Some def -> (hyps,(id,def)::subst,rmv)
-            | None -> (hyps,subst,id::rmv)
+          (hyps,id::rmv)
         else begin
-          let d' =
-            (id, option_app (replace_vars subst) c, replace_vars subst ty) in
-          check_clear_forward rmv (global_vars_set_of_decl env d')
+          check_clear_forward rmv (global_vars_set_of_decl env d)
             ("hypothesis "^string_of_id id);
-          (add_named_decl d' hyps, subst, rmv)
+          (add_named_decl d hyps, rmv)
         end)
       gl.evar_hyps
-      ~init:(empty_named_context,[],[]) in
-  let ncl = replace_vars subst gl.evar_concl in
+      ~init:(empty_named_context,[]) in
+  let ncl = gl.evar_concl in
   check_clear_forward rmv (global_vars_set env ncl) "conclusion";
   mk_goal nhyps ncl