diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 16 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 10 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 25 |
3 files changed, 35 insertions, 16 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 14d0c04212..72e6006b7e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -483,7 +483,10 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos g = (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))) ; (* Then the equation itself *) - Proofview.V82.of_tactic (intro_using heq_id) + Proofview.V82.of_tactic + (intro_using_then heq_id + (* we get the fresh name with onLastHypId *) + (fun _ -> Proofview.tclUNIT ())) ; onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) @@ -864,7 +867,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma in let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent + ~idopt:None in evd @@ -1112,16 +1116,18 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num in let first_tac : tactic = (* every operations until fix creations *) + (* names are already refreshed *) tclTHENLIST [ observe_tac "introducing params" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.params))) + (intros_mustbe_force (List.rev_map id_of_decl princ_info.params))) ; observe_tac "introducing predictes" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.predicates))) + (intros_mustbe_force + (List.rev_map id_of_decl princ_info.predicates))) ; observe_tac "introducing branches" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.branches))) + (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches))) ; observe_tac "building fixes" mk_fixes ] in let intros_after_fixes : tactic = diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index ffce2f8c85..45b1713441 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1526,9 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lemma = fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma in - let (_ : GlobRef.t list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent - ~idopt:None + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma + ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with @@ -1599,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) lemma) in let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent - ~idopt:None + Declare.Proof.save_regular ~proof:lemma + ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 64f62ba1fb..066ade07d2 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -59,7 +59,8 @@ let declare_fun name kind ?univs value = let defined lemma = let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent + ~idopt:None in () @@ -413,7 +414,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = observe_tclTHENLIST (fun _ _ -> str "treat_case1") [ h_intros (List.rev rev_ids) - ; Proofview.V82.of_tactic (intro_using teq_id) + ; Proofview.V82.of_tactic + (intro_using_then teq_id (fun _ -> Proofview.tclUNIT ())) ; onLastHypId (fun heq -> observe_tclTHENLIST (fun _ _ -> str "treat_case2") @@ -600,7 +602,11 @@ let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g = (Proofview.V82.of_tactic (simplest_case (mkVar id))) [ observe_tclTHENLIST (fun _ _ -> str "") - [ Proofview.V82.of_tactic (intro_using h_id) + [ Proofview.V82.of_tactic + (intro_using_then h_id + (* We don't care about the refreshed name, + accessed only through auto? *) + (fun _ -> Proofview.tclUNIT ())) ; Proofview.V82.of_tactic (simplest_elim (mkApp (delayed_force lt_n_O, [|s_max|]))) @@ -864,7 +870,10 @@ let terminate_app_rec (f, args) expr_info continuation_tac _ g = (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args)))) [ observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2") - [ Proofview.V82.of_tactic (intro_using rec_res_id) + [ Proofview.V82.of_tactic + (intro_using_then rec_res_id + (* refreshed name gotten from onNthHypId *) + (fun _ -> Proofview.tclUNIT ())) ; Proofview.V82.of_tactic intro ; onNthHypId 1 (fun v_bound -> onNthHypId 2 (fun v -> @@ -1503,7 +1512,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name in let lemma = build_proof env (Evd.from_env env) start_tac end_tac in let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None + Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None in () in @@ -1662,7 +1671,11 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref in let _ = Flags.silently - (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None) + (fun () -> + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None + in + ()) () in () |