diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/table.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 8 |
3 files changed, 6 insertions, 6 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 4e60696a81..ba21c6cbf1 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -656,7 +656,7 @@ let add_implicits r l = else err (int i ++ str " is not a valid argument number for " ++ safe_pr_global r) | ArgId id -> - (try List.index (Name id) names + (try List.index Name.equal (Name id) names with Not_found -> err (str "No argument " ++ pr_id id ++ str " for " ++ safe_pr_global r)) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 34b3728603..34814c350e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -379,7 +379,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas if Int.equal (List.length names) 1 then 1 else error "Recursive argument must be specified" | Some wf_arg -> - List.index (Name wf_arg) names + List.index Name.equal (Name wf_arg) names in let unbounded_eq = let f_app_args = diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 752fa45984..860a2524c2 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -223,7 +223,7 @@ let unintern_omega env id = calcul des variables utiles. *) let add_reified_atom t env = - try List.index0_f Term.eq_constr t env.terms + try List.index0 Term.eq_constr t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -234,7 +234,7 @@ let get_reified_atom env = (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) let add_prop env t = - try List.index0_f Term.eq_constr t env.props + try List.index0 Term.eq_constr t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i @@ -1039,7 +1039,7 @@ let mk_direction_list l = (* \section{Rejouer l'historique} *) let get_hyp env_hyp i = - try List.index0 (CCEqua i) env_hyp + try List.index0 Pervasives.(=) (CCEqua i) env_hyp with Not_found -> failwith (Printf.sprintf "get_hyp %d" i) let replay_history env env_hyp = @@ -1265,7 +1265,7 @@ let resolution env full_reified_goal systems_list = | ((O_left | O_mono) :: l) -> app coq_p_left [| loop l |] | (O_right :: l) -> app coq_p_right [| loop l |] in let correct_index = - let i = List.index0 e.e_origin.o_hyp l_hyps in + let i = List.index0 Names.Id.equal e.e_origin.o_hyp l_hyps in (* PL: it seems that additionnally introduced hyps are in the way during normalization, hence this index shifting... *) if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce) |