diff options
| author | Brian Campbell | 2019-03-21 19:03:56 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-21 19:17:01 +0000 |
| commit | b28dc3f4f74d02f5f0244ee3cee019bc1e4c7583 (patch) | |
| tree | 43a2659839a4749935d658d60983d1abd6bce5dd /src | |
| parent | 13ad54f450a11a9c4eecdd782036e50ea2a41cd8 (diff) | |
Coq: fix bug when multiple type variables map to the same identifier
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 632b5d02..cee9b89d 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1192,12 +1192,11 @@ let merge_new_tyvars ctxt old_env pat new_env = let remove_binding id (m,r) = match Bindings.find_opt id r with | Some kid -> -debug ctxt (lazy ("Removing " ^ string_of_kid kid ^ " to " ^ string_of_id id)); - KBindings.add kid None m, Bindings.remove id r + debug ctxt (lazy ("Removing " ^ string_of_kid kid ^ " to " ^ string_of_id id)); + KBindings.add kid None m, Bindings.remove id r | None -> m,r in let check_kid id kid (m,r) = - let m,r = remove_binding id (m,r) in try let _ = Env.get_typ_var kid old_env in debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); @@ -1215,7 +1214,7 @@ debug ctxt (lazy ("Removing " ^ string_of_kid kid ^ " to " ^ string_of_id id)); -> check_kid id kid m | _ -> debug ctxt (lazy (" not suitable type")); - remove_binding id m + m in let rec merge_pat m (P_aux (p,(l,_))) = match p with @@ -1229,7 +1228,7 @@ debug ctxt (lazy ("Removing " ^ string_of_kid kid ^ " to " ^ string_of_id id)); | P_var (p,ty_p) -> begin match p, ty_p with | _, TP_aux (TP_wild,_) -> merge_pat m p - | P_aux (P_id id,_), TP_aux (TP_var kid,_) -> check_kid id kid m + | P_aux (P_id id,_), TP_aux (TP_var kid,_) -> check_kid id kid (merge_pat m p) | _ -> merge_pat m p end (* Some of these don't make it through to the backend, but it's obvious what @@ -1244,7 +1243,8 @@ debug ctxt (lazy ("Removing " ^ string_of_kid kid ^ " to " ^ string_of_id id)); | P_record (fps,_) -> unreachable l __POS__ "Coq backend doesn't support record patterns properly yet" | P_cons (p1,p2) -> merge_pat (merge_pat m p1) p2 in - let m,r = merge_pat (ctxt.kid_id_renames, ctxt.kid_id_renames_rev) pat in + let m,r = IdSet.fold remove_binding (pat_ids pat) (ctxt.kid_id_renames, ctxt.kid_id_renames_rev) in + let m,r = merge_pat (m, r) pat in { ctxt with kid_id_renames = m; kid_id_renames_rev = r } let prefix_recordtype = true |