diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-27 19:20:27 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-27 19:20:27 +0000 |
| commit | 11ca3113365639136cf65a74c345080a9434e69b (patch) | |
| tree | da263c149cd1e90bde14768088730e48e78e4776 /plugins/firstorder/unify.ml | |
| parent | ee2f85396fa0cef65bc4295b5ac6c259e83df134 (diff) | |
Removing a bunch of generic equalities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/firstorder/unify.ml')
| -rw-r--r-- | plugins/firstorder/unify.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |