diff options
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0bbe4bb4c..3199474dd 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -16,6 +16,8 @@ open Libnames open Globnames open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* let msgnl = Pp.msgnl *) (* @@ -307,7 +309,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun)) + (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -938,8 +940,8 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl decl = Nameops.out_name (get_name decl) -let var_of_decl decl = mkVar (id_of_decl decl) +let id_of_decl = RelDecl.get_name %> Nameops.out_name +let var_of_decl = id_of_decl %> mkVar let revert idl = tclTHEN (Proofview.V82.of_tactic (generalize (List.map mkVar idl))) @@ -1072,7 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Name new_id) ) in - let fresh_decl = map_name fresh_id in + let fresh_decl = RelDecl.map_name fresh_id in let princ_info : elim_scheme = { princ_info with params = List.map fresh_decl princ_info.params; @@ -1119,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) + prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) + prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1165,7 +1167,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let pte_to_fix,rev_info = List.fold_left_i (fun i (acc_map,acc_info) decl -> - let pte = get_name decl in + let pte = RelDecl.get_name decl in let infos = info_array.(i) in let type_args,_ = decompose_prod infos.types in let nargs = List.length type_args in @@ -1276,7 +1278,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params)) + (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs @@ -1555,7 +1557,7 @@ let prove_principle_for_gen | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) - let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in + let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in @@ -1583,7 +1585,7 @@ let prove_principle_for_gen ) g in - let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in + let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in let lemma = match !tcc_lemma_ref with | None -> error "No tcc proof !!" @@ -1630,7 +1632,7 @@ let prove_principle_for_gen [ observe_tac "start_tac" start_tac; h_intros - (List.rev_map (fun decl -> Nameops.out_name (get_name decl)) + (List.rev_map (get_name %> Nameops.out_name) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by @@ -1668,7 +1670,7 @@ let prove_principle_for_gen in let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in let predicates_names = - List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates + List.map (get_name %> Nameops.out_name) princ_info.predicates in let pte_info = { proving_tac = @@ -1684,7 +1686,7 @@ let prove_principle_for_gen is_mes acc_inv fix_id (!tcc_list@(List.map - (fun decl -> (Nameops.out_name (get_name decl))) + (get_name %> Nameops.out_name) (princ_info.args@princ_info.params) )@ ([acc_rec_arg_id])) eqs ) @@ -1713,7 +1715,7 @@ let prove_principle_for_gen (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof - (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches) + (List.map (get_name %> Nameops.out_name) princ_info.branches) (List.rev args_ids) ) gl' |