aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-27 00:09:59 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-27 00:27:14 +0200
commit775fefc7ca57cee1b3b8a368ac26492dbe5a8910 (patch)
treedb480494456d8a072fa75c7ad6196986a70c4640 /engine
parentb9740771e8113cb9e607793887be7a12587d0326 (diff)
Fixing an old bug in collecting evars with cleared context.
The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
Diffstat (limited to 'engine')
-rw-r--r--engine/proofview.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index eef2b83f4..598358c47 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -153,8 +153,12 @@ let focus i j sp =
( { sp with comb = new_comb } , context )
(** [undefined defs l] is the list of goals in [l] which are still
- unsolved (after advancing cleared goals). *)
-let undefined defs l = CList.map_filter (Evarutil.advance defs) l
+ unsolved (after advancing cleared goals). Note that order matters. *)
+let undefined defs l =
+ List.fold_right (fun evk l ->
+ match Evarutil.advance defs evk with
+ | Some evk -> List.add_set Evar.equal evk l
+ | None -> l) l []
(** Unfocuses a proofview with respect to a context. *)
let unfocus c sp =