let set =
List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
in
- (*EqualitySet.elements set*) eq_list, set (* see applys.ma *)
+ (* we have the invariant that the list and the set have the same
+ * cardinality *)
+ EqualitySet.elements set, set
;;
+
let make_empty_active () = [], Indexing.empty ;;
let make_active eq_list =
eq_list, List.fold_left Indexing.index Indexing.empty eq_list
let size_of_passive (passive_list, _) = List.length passive_list;;
let size_of_active (active_list, _) = List.length active_list;;
+
let passive_is_empty = function
| [], s when EqualitySet.is_empty s -> true
| [], s -> assert false (* the set and the list should be in sync *)
status goalproof newproof subsumption_id subsumption_subst proof_menv
in
let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
- let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
+ let newmetasenv =
+ other_menv @
+ List.filter
+ (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+ in
+ let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
(subst, proof,gl)) subsumed_or_id
in
res, !maxmeta