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.

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 ->