diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:07 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:07 +0000 |
commit | 5e6145c871eea1e94566b252b4bfc4cd752f42d5 (patch) | |
tree | 97dfa98357cb0cf90bf06c9d470e6788de84c3b1 /toplevel | |
parent | 9b56e832ef591379dd1f2b29fe7d88513f7caf50 (diff) |
cList: set-as-list functions are now with an explicit comparison
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/command.ml | 33 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 4 |
3 files changed, 20 insertions, 19 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 1dbdcf78c..127d1d76e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -260,17 +260,17 @@ let minductive_message = function let check_all_names_different indl = let ind_names = List.map (fun ind -> ind.ind_name) indl in let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in - let l = List.duplicates ind_names in + let l = List.duplicates Id.equal ind_names in let () = match l with | [] -> () | t :: _ -> raise (InductiveError (SameNamesTypes t)) in - let l = List.duplicates cstr_names in + let l = List.duplicates Id.equal cstr_names in let () = match l with | [] -> () | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l))) in - let l = List.intersect ind_names cstr_names in + let l = List.intersect Id.equal ind_names cstr_names in match l with | [] -> () | _ -> raise (InductiveError (SameNamesOverlap l)) @@ -436,36 +436,37 @@ let do_mutual_inductive indl finite = partial_order : ('a * 'a list) list -> ('a * ('a,'a list) union) list *) -let rec partial_order = function +let rec partial_order cmp = function | [] -> [] | (x,xge)::rest -> let rec browse res xge' = function | [] -> let res = List.map (function - | (z, Inr zge) when List.mem x zge -> (z, Inr (List.union zge xge')) + | (z, Inr zge) when List.mem_f cmp x zge -> + (z, Inr (List.union cmp zge xge')) | r -> r) res in (x,Inr xge')::res | y::xge -> let rec link y = - try match List.assoc y res with + try match List.assoc_f cmp y res with | Inl z -> link z | Inr yge -> - if List.mem x yge then - let res = List.remove_assoc y res in + if List.mem_f cmp x yge then + let res = List.remove_assoc_f cmp y res in let res = List.map (function | (z, Inl t) -> - if Id.equal t y then (z, Inl x) else (z, Inl t) + if cmp t y then (z, Inl x) else (z, Inl t) | (z, Inr zge) -> - if List.mem y zge then - (z, Inr (List.add_set x (List.remove y zge))) + if List.mem_f cmp y zge then + (z, Inr (List.add_set cmp x (List.remove cmp y zge))) else (z, Inr zge)) res in - browse ((y,Inl x)::res) xge' (List.union xge (List.remove x yge)) + browse ((y,Inl x)::res) xge' (List.union cmp xge (List.remove cmp x yge)) else - browse res (List.add_set y (List.union xge' yge)) xge - with Not_found -> browse res (List.add_set y xge') xge + browse res (List.add_set cmp y (List.union cmp xge' yge)) xge + with Not_found -> browse res (List.add_set cmp y xge') xge in link y - in browse (partial_order rest) [] xge + in browse (partial_order cmp rest) [] xge let non_full_mutual_message x xge y yge isfix rest = let reason = @@ -490,7 +491,7 @@ let check_mutuality env isfix fixl = List.map (fun (id,def) -> (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env id' def) names)) fixl in - let po = partial_order preorder in + let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with | (x,Inr xge)::(y,Inr yge)::rest -> msg_warning (non_full_mutual_message x xge y yge isfix rest) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e9fd0620d..231f764c5 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -391,7 +391,7 @@ let analyze_notation_tokens l = let l = raw_analyze_notation_tokens l in let vars = get_notation_vars l in let recvars,l = interp_list_parser [] l in - recvars, List.subtract vars (List.map snd recvars), l + recvars, List.subtract Id.equal vars (List.map snd recvars), l let error_not_same_scope x y = error ("Variables "^Id.to_string x^" and "^Id.to_string y^ diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index eb4038721..fd4ac4890 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -171,8 +171,8 @@ let print_modules () = and loaded = Library.loaded_libraries () in (* we intersect over opened to preserve the order of opened since *) (* non-commutative operations (e.g. visibility) are done at import time *) - let loaded_opened = List.intersect opened loaded - and only_loaded = List.subtract loaded opened in + let loaded_opened = List.intersect DirPath.equal opened loaded + and only_loaded = List.subtract DirPath.equal loaded opened in str"Loaded and imported library files: " ++ pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++ str"Loaded and not imported library files: " ++ |