diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-31 19:17:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-31 19:17:47 +0000 |
| commit | 0721090dea4d9018f4c4cad8cefa1a10fb0d5a71 (patch) | |
| tree | e5d33456ca9e2e98b7cfcc952b834235250f3aa1 /pretyping | |
| parent | 736294486e4d5a4238c98af1ba35e20e59215ee2 (diff) | |
Corrige un bug du commit 11187 (le comportement à respecter était
celui-là: si une structure canonique existe déjà avec une certaine
projection canonique donnée, on garde l'ancienne structure si jamais
une structure canonique plus récente arrive avec la même projection
canonique).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11298 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/recordops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 100109652..110e4fe59 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -186,8 +186,8 @@ let open_canonical_structure i (_,o) = let lo = compute_canonical_projections o in List.iter (fun ((proj,cs_pat),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in - let l' = list_add_set (cs_pat,s) l in - object_table := Refmap.add proj l' !object_table) lo + if not (List.mem_assoc cs_pat l) then + object_table := Refmap.add proj ((cs_pat,s)::l) !object_table) lo let cache_canonical_structure o = open_canonical_structure 1 o |