From 11ca3113365639136cf65a74c345080a9434e69b Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 27 Sep 2013 19:20:27 +0000 Subject: Removing a bunch of generic equalities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/firstorder/sequent.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder/sequent.ml') 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= -- cgit v1.2.3