diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-06-20 08:09:00 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-20 08:09:00 +0200 |
commit | 25cd7acea0df79fcc07274e429c9839de1246611 (patch) | |
tree | 1ee95df49ec9ea7152afed41df425ea4e4760736 /plugins/funind | |
parent | c7ac5dc8036623a02ab4ad6d11469e040e78c004 (diff) | |
parent | 0437339ccac602d692b5b8c071b77ac756805520 (diff) |
Merge PR#803: Clean ssr
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.mli | 4 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.mli | 2 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 4 | ||||
-rw-r--r-- | plugins/funind/indfun.mli | 2 | ||||
-rw-r--r-- | plugins/funind/indfun_common.mli | 4 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 10 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
-rw-r--r-- | plugins/funind/recdef.mli | 4 |
9 files changed, 17 insertions, 18 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ef894b239..ba46f78aa 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -10,7 +10,6 @@ open Names open Pp open Tacmach open Termops -open Proof_type open Tacticals open Tactics open Indfun_common @@ -106,7 +105,7 @@ let make_refl_eq constructor type_of_t t = type pte_info = { - proving_tac : (Id.t list -> Proof_type.tactic); + proving_tac : (Id.t list -> Tacmach.tactic); is_valid : constr -> bool } diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 5bb288678..d03fc475e 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -4,7 +4,7 @@ open Names val prove_princ_for_struct : Evd.evar_map ref -> bool -> - int -> Constant.t array -> EConstr.constr array -> int -> Proof_type.tactic + int -> Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic val prove_principle_for_gen : @@ -14,7 +14,7 @@ val prove_principle_for_gen : int -> (* the number of recursive argument *) EConstr.types -> (* the type of the recursive argument *) EConstr.constr -> (* the wf relation used to prove the function *) - Proof_type.tactic + Tacmach.tactic (* val is_pte : rel_declaration -> bool *) diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index bb2b2d918..e70ef2365 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -28,7 +28,7 @@ val generate_functional_principle : (* The tactic to use to make the proof w.r the number of params *) - (EConstr.constr array -> int -> Proof_type.tactic) -> + (EConstr.constr array -> int -> Tacmach.tactic) -> unit val compute_new_princ_type_from_rel : constr array -> Sorts.t array -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d12aa7f42..ad04e430c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -343,7 +343,7 @@ let error_error names e = let generate_principle (evd:Evd.evar_map ref) pconstants on_error is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> - Proof_type.tactic) : unit = + Tacmach.tactic) : unit = let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in @@ -446,7 +446,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation - (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic = + (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic = Functional_principles_proofs.prove_principle_for_gen (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 33420d813..fc7da6a33 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -16,7 +16,7 @@ val functional_induction : EConstr.constr -> (EConstr.constr * EConstr.constr bindings) option -> Tacexpr.or_and_intro_pattern option -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val make_graph : Globnames.global_reference -> unit diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 6b40c9171..f7a9cedd7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -105,7 +105,7 @@ exception ToShow of exn val is_strict_tcc : unit -> bool -val h_intros: Names.Id.t list -> Proof_type.tactic +val h_intros: Names.Id.t list -> Tacmach.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed @@ -114,7 +114,7 @@ val well_founded_ltof : EConstr.constr Util.delayed val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference -val list_rewrite : bool -> (EConstr.constr*bool) list -> Proof_type.tactic +val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ebdb490e3..94ef2590c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -218,7 +218,7 @@ let rec generate_fresh_id x avoid i = \end{enumerate} *) -let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Proof_type.tactic = +let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: @@ -468,7 +468,7 @@ let tauto = let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g -and intros_with_rewrite_aux : Proof_type.tactic = +and intros_with_rewrite_aux : Tacmach.tactic = fun g -> let eq_ind = make_eq () in let sigma = project g in @@ -629,7 +629,7 @@ let rec reflexivity_with_destruct_cases g = *) -let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.tactic = +let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* We compute the types of the different mutually recursive lemmas in $\zeta$ normal form @@ -673,7 +673,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.ta using [f_equation] if it is recursive (that is the graph is infinite or unfold if the graph is finite *) - let rewrite_tac j ids : Proof_type.tactic = + let rewrite_tac j ids : Tacmach.tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) @@ -953,7 +953,7 @@ let revert_graph kn post_tac hid g = \end{enumerate} *) -let functional_inversion kn hid fconst f_correct : Proof_type.tactic = +let functional_inversion kn hid fconst f_correct : Tacmach.tactic = fun g -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in let sigma = project g in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3cd20a950..8e12b239e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -30,7 +30,7 @@ open Nametab open Declare open Decl_kinds open Tacred -open Proof_type +open Goal open Pfedit open Glob_term open Pretyping diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index e1a072799..f3d5e7332 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -2,10 +2,10 @@ open API (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : - Proof_type.tactic -> + Tacmach.tactic -> bool -> Names.Id.t list option -> - Proof_type.tactic + Tacmach.tactic val recursive_definition : bool -> Names.Id.t -> |