diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 3 |
5 files changed, 7 insertions, 6 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index aaf6f2bd09..9fe5606b97 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -152,7 +152,7 @@ let factor_fix env l cb msb = if List.length msb < n-1 then raise Impossible; let msb', msb'' = List.chop (n-1) msb in let labels = Array.make n l in - List.iter_i + List.iteri (fun j -> function | (l,SFBconst cb') -> diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 01b98b1312..e3abab82b3 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -969,7 +969,7 @@ and simpl_case o typ br e = else ([], Pwild, ast_pop f) in let brl = Array.to_list br in - let brl_opt = List.filter_i (fun i _ -> not (Intset.mem i ints)) brl in + let brl_opt = List.filteri (fun i _ -> not (Intset.mem i ints)) brl in let brl_opt = brl_opt @ [last_br] in MLcase (typ, e, Array.of_list brl_opt) | None -> MLcase (typ, e, br) @@ -1164,7 +1164,7 @@ let general_optimize_fix f ids n args m c = | MLrel j when v.(j-1)>=0 -> if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1) | _ -> raise Impossible - in List.iter_i aux args; + in List.iteri aux args; let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 6151abf6eb..4322ac95fa 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -877,7 +877,7 @@ let extract_inductive r s l optstr = Lib.add_anonymous_leaf (in_customs (g,[],s)); Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s))) optstr; - List.iter_i + List.iteri (fun j s -> let g = ConstructRef (ip,succ j) in Lib.add_anonymous_leaf (inline_extraction (true,[g])); diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 490d52555c..b820489f53 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1238,7 +1238,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b let l = ref [] in let _ = try - List.iter_i + List.iteri (fun i ((n,nt,is_defined) as param) -> if Array.for_all (fun l -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d8255e8342..bbc9ff93b3 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -122,10 +122,11 @@ let generate_type g_to_f f graph i = | _ -> let j = !i in incr i;mkRel (nb_args - j + 1) in (*i We need to name the vars [res] and [fv] i*) + let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in let res_id = Namegen.next_ident_away_in_goal (id_of_string "res") - (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt) + (List.map_filter filter fun_ctxt) in let fv_id = Namegen.next_ident_away_in_goal |