diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index ad435eb5..86e02623 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: environ.ml 11001 2008-05-27 16:56:07Z aspiwack $ *) +(* $Id: environ.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -379,17 +379,14 @@ let insert_after_hyp (ctxt,vals) id d check = (* To be used in Logic.clear_hyps *) let remove_hyps ids check_context check_value (ctxt, vals) = - let ctxt,vals,rmv = - List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals,rmv) -> + List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) -> if List.mem id ids then - (ctxt,vals,id::rmv) + (ctxt,vals) else let nd = check_context d in let nv = check_value v in - (nd::ctxt,(id',nv)::vals,rmv)) - ctxt vals ([],[],[]) - in ((ctxt,vals),rmv) - + (nd::ctxt,(id',nv)::vals)) + ctxt vals ([],[]) |