diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/formula.ml | 10 | ||||
| -rw-r--r-- | plugins/firstorder/instances.ml | 8 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.ml | 4 | ||||
| -rw-r--r-- | plugins/firstorder/unify.ml | 6 |
4 files changed, 14 insertions, 14 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 89ba7b259..03a832e90 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -22,11 +22,11 @@ let red_flags=ref Closure.betaiotazeta let (=?) f g i1 i2 j1 j2= let c=f i1 i2 in - if c=0 then g j1 j2 else c + if Int.equal c 0 then g j1 j2 else c let (==?) fg h i1 i2 j1 j2 k1 k2= let c=fg i1 i2 j1 j2 in - if c=0 then h k1 k2 else c + if Int.equal c 0 then h k1 k2 else c type ('a,'b) sum = Left of 'a | Right of 'b @@ -88,20 +88,20 @@ let kind_of_formula gl term = let ind=destInd i in let (mib,mip) = Global.lookup_inductive ind in let nconstr=Array.length mip.mind_consnames in - if nconstr=0 then + if Int.equal nconstr 0 then False(ind,l) else let has_realargs=(n>0) in let is_trivial= let is_constant c = - nb_prod c = mib.mind_nparams in + Int.equal (nb_prod c) mib.mind_nparams in Array.exists is_constant mip.mind_nf_lc in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then Atom cciterm else - if nconstr=1 then + if Int.equal nconstr 1 then And(ind,l,is_trivial) else Or(ind,l,is_trivial) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 4b15dcae5..ac612d0cd 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -30,8 +30,8 @@ let compare_instance inst1 inst2= (OrderedConstr.compare d1 d2) | Real((m1,c1),n1),Real((m2,c2),n2)-> ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2 - | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1 - | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 + | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1 + | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1 let compare_gr id1 id2 = if id1==id2 then 0 else @@ -115,13 +115,13 @@ let mk_open_instance id gl m t= | Anonymous -> dummy_bvid in let revt=substl (List.init m (fun i->mkRel (m-i))) t in let rec aux n avoid= - if n=0 then [] else + if Int.equal n 0 then [] else let nid=(fresh_id avoid var_id gl) in (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in let nt=it_mkLambda_or_LetIn revt (aux m []) in let rawt=Detyping.detype false [] [] nt in let rec raux n t= - if n=0 then t else + if Int.equal n 0 then t else match t with GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in 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= diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index e59f0419e..eeaf270c3 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -42,7 +42,7 @@ let unif t1 t2= and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in match (kind_of_term nt1),(kind_of_term nt2) with Meta i,Meta j-> - if i<>j then + if not (Int.equal i j) then if i<j then bind j nt1 else bind i nt2 | Meta i,_ -> @@ -63,7 +63,7 @@ let unif t1 t2= Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; let l=Array.length va in - if l<>(Array.length vb) then + if not (Int.equal l (Array.length vb)) then raise (UFAIL (nt1,nt2)) else for i=0 to l-1 do @@ -72,7 +72,7 @@ let unif t1 t2= | App(ha,va),App(hb,vb)-> Queue.add (ha,hb) bige; let l=Array.length va in - if l<>(Array.length vb) then + if not (Int.equal l (Array.length vb)) then raise (UFAIL (nt1,nt2)) else for i=0 to l-1 do |