diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 10:56:41 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 10:56:41 +0000 |
| commit | 9a0c61b81a2d9c0024b20a6c7ad8af01026739b0 (patch) | |
| tree | 36d6f581d692180f12d52f872da4d35662aee2ab /plugins/firstorder | |
| parent | 9330bf650ca602884c5c4c69c2fb3e94ee32838b (diff) | |
Moved Intset and Intmap to Int namespace.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/unify.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index f823cfa55..93f84687e 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -46,12 +46,12 @@ let unif t1 t2= else bind i nt2 | Meta i,_ -> let t=subst_meta !sigma nt2 in - if Intset.is_empty (free_rels t) && + if Int.Set.is_empty (free_rels t) && not (occur_term (mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in - if Intset.is_empty (free_rels t) && + if Int.Set.is_empty (free_rels t) && not (occur_term (mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige |