diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 12 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 25 |
3 files changed, 21 insertions, 22 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 79f311e282..afe89aef6e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -854,10 +854,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) let info = Declare.Info.make () in - let lemma = - Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info - ~impargs:[] evd lemma_type + let cinfo = + Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type () in + let lemma = Declare.Proof.start ~cinfo ~info evd in let lemma, _ = Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma in diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 50ce783579..0cd5df12f7 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1519,10 +1519,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lem_id = mk_correct_id f_id in let typ, _ = lemmas_types_infos.(i) in let info = Declare.Info.make () in - let lemma = - Declare.Proof.start ~name:lem_id ~poly:false ~info ~impargs:[] !evd - typ - in + let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in + let lemma = Declare.Proof.start ~cinfo ~info !evd in let lemma = fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma in @@ -1585,10 +1583,10 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) i*) let lem_id = mk_complete_id f_id in let info = Declare.Info.make () in - let lemma = - Declare.Proof.start ~name:lem_id ~poly:false sigma ~info ~impargs:[] - (fst lemmas_types_infos.(i)) + let cinfo = + Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) () in + let lemma = Declare.Proof.start ~cinfo sigma ~info in let lemma = fst (Declare.Proof.by diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5a188ca82b..92eb85ffd8 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1492,10 +1492,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None in let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in - let lemma = - Declare.Proof.start ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma - gls_type - in + let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type () in + let lemma = Declare.Proof.start ~cinfo ~info sigma in let lemma = if Indfun_common.is_strict_tcc () then fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma @@ -1530,12 +1528,13 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes fonctional_ref input_type relation rec_arg_num thm_name using_lemmas nb_args ctx hook = let start_proof env ctx tac_start tac_end = - let info = Declare.Info.make ~hook () in - let lemma = - Declare.Proof.start ~name:thm_name ~poly:false (*FIXME*) ~info ctx - ~impargs:[] - (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) + let cinfo = + Declare.CInfo.make ~name:thm_name + ~typ:(EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) + () in + let info = Declare.Info.make ~hook () in + let lemma = Declare.Proof.start ~cinfo ~info ctx in let lemma = fst @@ Declare.Proof.by @@ -1605,10 +1604,12 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in let info = Declare.Info.make () in - let lemma = - Declare.Proof.start ~name:eq_name ~poly:false evd ~info ~impargs:[] - (EConstr.of_constr equation_lemma_type) + let cinfo = + Declare.CInfo.make ~name:eq_name + ~typ:(EConstr.of_constr equation_lemma_type) + () in + let lemma = Declare.Proof.start ~cinfo evd ~info in let lemma = fst @@ Declare.Proof.by |