diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 70 |
1 files changed, 35 insertions, 35 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a2f16dc6d..28752fe4f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -51,11 +51,11 @@ let coq_base_constant s = let find_reference sl s = (locate (make_qualid(Names.make_dirpath - (List.map id_of_string (List.rev sl))) - (id_of_string s)));; + (List.map Id.of_string (List.rev sl))) + (Id.of_string s)));; -let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = +let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = fun f_id kind value -> let ce = {const_entry_body = value; const_entry_secctx = None; @@ -73,7 +73,7 @@ let def_of_const t = | _ -> assert false) with _ -> anomaly ("Cannot find definition of constant "^ - (string_of_id (id_of_label (con_label sp)))) + (Id.to_string (id_of_label (con_label sp)))) ) |_ -> assert false @@ -86,8 +86,8 @@ let type_of_const t = let constant sl s = constr_of_global (locate (make_qualid(Names.make_dirpath - (List.map id_of_string (List.rev sl))) - (id_of_string s)));; + (List.map Id.of_string (List.rev sl))) + (Id.of_string s)));; let const_of_ref = function ConstRef kn -> kn | _ -> anomaly "ConstRef expected" @@ -120,15 +120,15 @@ let pf_get_new_ids idl g = let compute_renamed_type gls c = rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] (pf_type_of gls c) -let h'_id = id_of_string "h'" -let teq_id = id_of_string "teq" -let ano_id = id_of_string "anonymous" -let x_id = id_of_string "x" -let k_id = id_of_string "k" -let v_id = id_of_string "v" -let def_id = id_of_string "def" -let p_id = id_of_string "p" -let rec_res_id = id_of_string "rec_res";; +let h'_id = Id.of_string "h'" +let teq_id = Id.of_string "teq" +let ano_id = Id.of_string "anonymous" +let x_id = Id.of_string "x" +let k_id = Id.of_string "k" +let v_id = Id.of_string "v" +let def_id = Id.of_string "def" +let p_id = Id.of_string "p" +let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_base_constant "lt") let le = function () -> (coq_base_constant "le") let ex = function () -> (coq_base_constant "ex") @@ -202,7 +202,7 @@ let (value_f:constr list -> global_reference -> constr) = let body = understand Evd.empty env glob_body in it_mkLambda_or_LetIn body context -let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -300,7 +300,7 @@ let check_not_nested forbidden e = let rec check_not_nested e = match kind_of_term e with | Rel _ -> () - | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^string_of_id x) + | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^Id.to_string x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b @@ -324,21 +324,21 @@ let check_not_nested forbidden e = type 'a infos = { nb_arg : int; (* function number of arguments *) concl_tac : tactic; (* final tactic to finish proofs *) - rec_arg_id : identifier; (*name of the declared recursive argument *) + rec_arg_id : Id.t; (*name of the declared recursive argument *) is_mes : bool; (* type of recursion *) - ih : identifier; (* induction hypothesis name *) - f_id : identifier; (* function name *) + ih : Id.t; (* induction hypothesis name *) + f_id : Id.t; (* function name *) f_constr : constr; (* function term *) f_terminate : constr; (* termination proof term *) func : global_reference; (* functionnal reference *) info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) - values_and_bounds : (identifier*identifier) list; - eqs : identifier list; - forbidden_ids : identifier list; + values_and_bounds : (Id.t*Id.t) list; + eqs : Id.t list; + forbidden_ids : Id.t list; acc_inv : constr lazy_t; - acc_id : identifier; + acc_id : Id.t; args_assoc : ((constr list)*constr) list; } @@ -651,7 +651,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = introduced back later; the result is the pair of the tactic and the list of hypotheses that have been generalized and cleared. *) let mkDestructEq : - identifier list -> constr -> goal sigma -> tactic * identifier list = + Id.t list -> constr -> goal sigma -> tactic * Id.t list = fun not_on_hyp expr g -> let hyps = pf_hyps g in let to_revert = @@ -1031,10 +1031,10 @@ let termination_proof_header is_mes input_type ids args_id relation in let relation = substl pre_rec_args relation in let input_type = substl pre_rec_args input_type in - let wf_thm = next_ident_away_in_goal (id_of_string ("wf_R")) ids in + let wf_thm = next_ident_away_in_goal (Id.of_string ("wf_R")) ids in let wf_rec_arg = next_ident_away_in_goal - (id_of_string ("Acc_"^(string_of_id rec_arg_id))) + (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))) (wf_thm::ids) in let hrec = next_ident_away_in_goal hrec_id @@ -1206,8 +1206,8 @@ let build_and_l l = let is_rec_res id = - let rec_res_name = string_of_id rec_res_id in - let id_name = string_of_id id in + let rec_res_name = Id.to_string rec_res_id in + let id_name = Id.to_string id in try String.sub id_name 0 (String.length rec_res_name) = rec_res_name with _ -> false @@ -1384,7 +1384,7 @@ let com_terminate let start_equation (f:global_reference) (term_f:global_reference) - (cont_tactic:identifier list -> tactic) g = + (cont_tactic:Id.t list -> tactic) g = let ids = pf_ids_of_hyps g in let terminate_constr = constr_of_global term_f in let nargs = nb_prod (type_of_const terminate_constr) in @@ -1397,7 +1397,7 @@ let start_equation (f:global_reference) (term_f:global_reference) Array.of_list (List.map mkVar x)))); observe_tac (str "prove_eq") (cont_tactic x)] g;; -let (com_eqn : int -> identifier -> +let (com_eqn : int -> Id.t -> global_reference -> global_reference -> global_reference -> constr -> unit) = fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> @@ -1430,12 +1430,12 @@ let (com_eqn : int -> identifier -> eqs = []; forbidden_ids = []; acc_inv = lazy (assert false); - acc_id = id_of_string "____"; + acc_id = Id.of_string "____"; args_assoc = []; - f_id = id_of_string "______"; - rec_arg_id = id_of_string "______"; + f_id = Id.of_string "______"; + rec_arg_id = Id.of_string "______"; is_mes = false; - ih = id_of_string "______"; + ih = Id.of_string "______"; } ) ); |