diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
6 files changed, 13 insertions, 13 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ca73799c18..9c895e6a9c 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -966,7 +966,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in - let f_id = id_of_label (con_label (destConst f)) in + let f_id = Label.to_id (con_label (destConst f)) in let prove_replacement = tclTHENSEQ [ @@ -1000,7 +1000,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let finfos = find_Function_infos (destConst f) in mkConst (Option.get finfos.equation_lemma) with (Not_found | Option.IsNone as e) -> - let f_id = id_of_label (con_label (destConst f)) in + let f_id = Label.to_id (con_label (destConst f)) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious i*) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1d30ce9a63..9678fb547b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,14 +322,14 @@ let generate_functional_principle match new_princ_name with | Some (id) -> id,id | None -> - let id_of_f = id_of_label (con_label f) in + let id_of_f = Label.to_id (con_label f) in id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in let names = ref [new_princ_name] in let hook new_principle_type _ _ = if sorts = None then - (* let id_of_f = id_of_label (con_label f) in *) + (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = let s = Termops.new_sort_in_family fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in @@ -390,7 +390,7 @@ let get_funs_constant mp dp = (fun i na -> match na with | Name id -> - let const = make_con mp dp (label_of_id id) in + let const = make_con mp dp (Label.of_id id) in const,i | Anonymous -> anomaly "Anonymous fix" diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dfce8bf48..6c3b009f85 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -58,7 +58,7 @@ let functional_induction with_clean c princl pat = (or f_rec, f_rect) i*) let princ_name = Indrec.make_elimination_ident - (id_of_label (con_label c')) + (Label.to_id (con_label c')) (Tacticals.elimination_sort_of_goal g) in try @@ -810,14 +810,14 @@ let make_graph (f_ref:global_reference) = in l | _ -> - let id = id_of_label (con_label c) in + let id = Label.to_id (con_label c) in [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in do_generate_principle error_error false false expr_list; (* We register the infos *) let mp,dp,_ = repr_con c in List.iter - (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (label_of_id id))) + (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) expr_list); Dumpglob.continue () diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5942e11b49..dfbfdce3a3 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -408,7 +408,7 @@ let update_Function finfo = let add_Function is_general f = - let f_id = id_of_label (con_label f) in + let f_id = Label.to_id (con_label f) in let equation_lemma = find_or_none (mk_equation_id f_id) and correctness_lemma = find_or_none (mk_correct_id f_id) and completeness_lemma = find_or_none (mk_complete_id f_id) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 4a466175f6..eed4211590 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -179,7 +179,7 @@ let find_induction_principle f = (* let fname = *) (* match kind_of_term f with *) (* | Const c' -> *) -(* id_of_label (con_label c') *) +(* Label.to_id (con_label c') *) (* | _ -> error "Must be used with a function" *) (* in *) @@ -1049,7 +1049,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g in Array.iteri (fun i f_as_constant -> - let f_id = id_of_label (con_label f_as_constant) in + let f_id = Label.to_id (con_label f_as_constant) in (*i The next call to mk_correct_id is valid since we are constructing the lemma Ensures by: obvious i*) @@ -1100,7 +1100,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g in Array.iteri (fun i f_as_constant -> - let f_id = id_of_label (con_label f_as_constant) in + let f_id = Label.to_id (con_label f_as_constant) in (*i The next call to mk_complete_id is valid since we are constructing the lemma Ensures by: obvious i*) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 68c5e16ae1..7b77afd072 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -73,7 +73,7 @@ let def_of_const t = | _ -> assert false) with _ -> anomaly ("Cannot find definition of constant "^ - (Id.to_string (id_of_label (con_label sp)))) + (Id.to_string (Label.to_id (con_label sp)))) ) |_ -> assert false |