From a7d95a6923960ad551314d3e72715f9ad766cffd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 20 Jun 2016 08:20:59 +0200 Subject: Fix bug #4825: [clear] should not dependency-check hypotheses that come above it. --- kernel/environ.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 9fb3bf79f..7d8c3c0af 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -538,20 +538,21 @@ 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 rec remove_hyps ctxt vals = match ctxt, vals with - | [], [] -> [], [] + | [], [] -> ([], []), false | d :: rctxt, (nid, v) :: rvals -> - let ans = remove_hyps rctxt rvals in - if Id.Set.mem (get_id d) ids then ans + let (ans, seen) = remove_hyps rctxt rvals in + if Id.Set.mem (get_id d) ids then (ans, true) + else if not seen then (ctxt, vals), false else let (rctxt', rvals') = ans in let d' = check_context d in let v' = check_value v in if d == d' && v == v' && rctxt == rctxt' && rvals == rvals' then - ctxt, vals - else (d' :: rctxt', (nid, v') :: rvals') + (ctxt, vals), true + else (d' :: rctxt', (nid, v') :: rvals'), true | _ -> assert false in - remove_hyps ctxt vals + fst (remove_hyps ctxt vals) (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module -- cgit v1.2.3