diff options
| author | ppedrot | 2012-09-15 00:39:54 +0000 |
|---|---|---|
| committer | ppedrot | 2012-09-15 00:39:54 +0000 |
| commit | 92616b9f660eaa2640964ca1925b05d37af70c8c (patch) | |
| tree | 52f433af85ee3bf8195b91f78ea60df75902f62d /toplevel | |
| parent | 8cc623262c625bda20e97c75f9ba083ae8e7760d (diff) | |
Some documentation and cleaning of CList and Util interfaces.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index c54dc81202..044502cda9 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -368,11 +368,11 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_,kn) = declare_mind isrecord mie in let mind = Global.mind_of_delta_kn kn in - List.iter_i (fun i (indimpls, constrimpls) -> + List.iteri (fun i (indimpls, constrimpls) -> let ind = (mind,i) in Autoinstance.search_declaration (IndRef ind); maybe_declare_manual_implicits false (IndRef ind) indimpls; - List.iter_i + List.iteri (fun j impls -> (* Autoinstance.search_declaration (ConstructRef (ind,j));*) maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) @@ -920,7 +920,7 @@ let do_program_recursive fixkind fixl ntns = in let indexes = Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in - List.iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl + List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl end; Obligations.add_mutual_definitions defs ntns fixkind |