diff options
| author | ppedrot | 2012-11-13 22:38:16 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-13 22:38:16 +0000 |
| commit | 98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 (patch) | |
| tree | e7ecad4d80598956e9aeda2f5c82302ab7e0bde8 /kernel/modops.ml | |
| parent | 1d436a18f2f72b57ea09a6d27709a36b63be863a (diff) | |
More monomorphizations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 1bef6bf50a..084628a4ef 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -138,10 +138,10 @@ let module_body_of_type mp mtb = mod_retroknowledge = []} let check_modpath_equiv env mp1 mp2 = - if mp1=mp2 then () else + if mp_eq mp1 mp2 then () else let mb1=lookup_module mp1 env in let mb2=lookup_module mp2 env in - if (mp_of_delta mb1.mod_delta mp1)=(mp_of_delta mb2.mod_delta mp2) + if mp_eq (mp_of_delta mb1.mod_delta mp1) (mp_of_delta mb2.mod_delta mp2) then () else error_not_equal_modpaths mp1 mp2 @@ -184,7 +184,7 @@ and subst_structure sub do_delta sign = and subst_module sub do_delta mb = let mp = subst_mp sub mb.mod_mp in - let sub = if is_functor mb.mod_type && not(mp=mb.mod_mp) then + let sub = if is_functor mb.mod_type && not (mp_eq mp mb.mod_mp) then add_mp mb.mod_mp mp empty_delta_resolver sub else sub in let id_delta = (fun x y-> x) in @@ -557,7 +557,7 @@ and clean_expr l = function | SEBfunctor (mbid,sigt,str) as s-> let str_clean = clean_expr l str in let sig_clean = clean_expr l sigt.typ_expr in - if str_clean == str && sig_clean = sigt.typ_expr then + if str_clean == str && Int.equal (Pervasives.compare sig_clean sigt.typ_expr) 0 then (** FIXME **) s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean) | SEBstruct str as s-> let str_clean = Util.List.smartmap (clean_struct l) str in |