diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-18 18:45:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-18 19:42:07 +0100 |
| commit | 410c088d3cb9f0e3fdb5c01cb036b95aae84a6c2 (patch) | |
| tree | 1ee5cde846c526f4ee5bcbbe78345939de65ae96 /checker/environ.ml | |
| parent | aefba30e028bf1774f01f95a69a6a75b80206a5f (diff) | |
Fixing checker with respect to new kernel name structure and hashmaps.
Some wrong generic equalities and hashes were removed too.
Diffstat (limited to 'checker/environ.ml')
| -rw-r--r-- | checker/environ.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index be6bdec11..eb084a910 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -126,8 +126,8 @@ let scrape_mind env kn= Not_found -> kn let mind_equiv env (kn1,i1) (kn2,i2) = - i1 = i2 && - scrape_mind env (user_mind kn1) = scrape_mind env (user_mind kn2) + Int.equal i1 i2 && + KerName.equal (scrape_mind env (user_mind kn1)) (scrape_mind env (user_mind kn2)) let lookup_mind kn env = @@ -139,7 +139,7 @@ let add_mind kn mib env = (string_of_mind kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = user_mind kn,canonical_mind kn in - let new_inds_eq = if kn1=kn2 then + let new_inds_eq = if KerName.equal kn1 kn2 then env.env_globals.env_inductives_eq else KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in |