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 /pretyping/unification.ml | |
| 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 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index bf0f47a32..facc243e2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -419,13 +419,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | Evar (evk,_ as ev), _ when not (ExistentialSet.mem evk flags.frozen_evars) -> let cmvars = free_rels cM and cnvars = free_rels cN in - if Intset.subset cnvars cmvars then + if Int.Set.subset cnvars cmvars then sigma,metasubst,((curenv,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) when not (ExistentialSet.mem evk flags.frozen_evars) -> let cmvars = free_rels cM and cnvars = free_rels cN in - if Intset.subset cmvars cnvars then + if Int.Set.subset cmvars cnvars then sigma,metasubst,((curenv,ev,cM)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | Sort s1, Sort s2 -> |