Achèvement correction bug do_restrict_hys: ne pas inverser les arguments

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

1 files changed, 2 insertions, 13 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2de116b612..b0aed65e17 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -240,20 +240,9 @@ let do_restrict_hyps evd ev args =
   let evi = Evd.map (evars_of !evd) ev in
   let env = evar_env evi in
   let hyps = evi.evar_hyps in
-  let (_,(rsign,ncargs)) =
-    List.fold_left 
-      (fun (sign,(rs,na)) a ->
-	 (List.tl sign,
-	  if not(closed0 a) then 
-	    (rs,na)
-	  else 
-	    (add_named_decl (List.hd sign) rs, a::na)))
-      (hyps,([],[])) args 
-  in
-  let sign' = List.rev rsign in
-  let env' = reset_with_named_context sign' env in
+  let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
   let (evd',nc) =
-    new_evar_instance sign' !evd evi.evar_concl
+    new_evar_instance sign !evd evi.evar_concl
       ~src:(evar_source ev !evd) ncargs in
   evd := Evd.evar_define ev nc evd';
   nc