diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-20 08:20:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-20 08:20:59 +0200 |
| commit | a7d95a6923960ad551314d3e72715f9ad766cffd (patch) | |
| tree | 548878c5ee8bb8bceccce85b90dc8d39f79bc805 /kernel/environ.ml | |
| parent | 43a43ea30b30e609ce28c69d50bc276c84073486 (diff) | |
Fix bug #4825: [clear] should not dependency-check hypotheses that come above it.
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 13 |
1 files changed, 7 insertions, 6 deletions
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 |