diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-06-15 16:41:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-06-16 10:27:47 +0200 |
| commit | 0437339ccac602d692b5b8c071b77ac756805520 (patch) | |
| tree | 755ba115f30cd91d067250468e5946dd1a0f4dc4 /plugins/funind/invfun.ml | |
| parent | 4f6fd16c06b9e11bc2619a34c1629bd71aba76de (diff) | |
Removing Proof_type from the API.
Unluckily, this forces replacing a lot of code in plugins, because the API
defined the type of goals and tactics in Proof_type, and by the no-alias rule,
this was the only one. But Proof_type was already implicitly deprecated, so
that the API should have relied on Tacmach instead.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 10 |
1 files changed, 5 insertions, 5 deletions
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 |