aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/sequent.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/sequent.ml')
-rw-r--r--plugins/firstorder/sequent.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 4e4a6f19f..8b831d595 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -88,7 +88,7 @@ let cm_add typ nam cm=
let cm_remove typ nam cm=
try
let l=CM.find typ cm in
- let l0=List.filter (fun id->id<>nam) l in
+ let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
match l0 with
[]->CM.remove typ cm
| _ ->CM.add typ l0 cm
@@ -118,7 +118,7 @@ let lookup item seq=
let p (id2,o)=
match o with
None -> false
- | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
+ | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in
History.exists p seq.history
let add_formula side nam t seq gl=