From 0437339ccac602d692b5b8c071b77ac756805520 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Jun 2017 16:41:09 +0200 Subject: 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. --- plugins/ssr/ssrast.mli | 4 +- plugins/ssr/ssrbwd.mli | 4 +- plugins/ssr/ssrcommon.ml | 2 +- plugins/ssr/ssrcommon.mli | 106 +++++++++++++++++++++---------------------- plugins/ssr/ssrelim.mli | 16 +++---- plugins/ssr/ssrequality.mli | 12 ++--- plugins/ssr/ssrfwd.mli | 6 +-- plugins/ssr/ssripats.ml | 6 +-- plugins/ssr/ssripats.mli | 16 +++---- plugins/ssr/ssrprinters.mli | 2 +- plugins/ssr/ssrtacticals.mli | 6 +-- plugins/ssr/ssrview.ml | 2 +- 12 files changed, 91 insertions(+), 91 deletions(-) (limited to 'plugins/ssr') diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 0f4b86d10..94eaa1d6a 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -145,6 +145,6 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option) (* OOP : these are general shortcuts *) type gist = Tacintern.glob_sign type ist = Tacinterp.interp_sign -type goal = Proof_type.goal +type goal = Goal.goal type 'a sigma = 'a Evd.sigma -type v82tac = Proof_type.tactic +type v82tac = Tacmach.tactic diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index b0e98bdb4..20a1263d2 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -10,7 +10,7 @@ open API -val apply_top_tac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma +val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val inner_ssrapplytac : Ssrast.ssrterm list -> @@ -19,4 +19,4 @@ val inner_ssrapplytac : list list -> Ssrast.ssrhyps -> Ssrast.ist -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index ded9fa66b..411ce6853 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -960,7 +960,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t)); - Tacmach.refine_no_check (EConstr.Unsafe.to_constr t) gl + Tacmach.refine_no_check t gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 7a4b47a46..f61168576 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -9,9 +9,9 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) open API +open Tacmach open Names open Environ -open Proof_type open Evd open Constrexpr open Ssrast @@ -122,11 +122,11 @@ val intern_term : ssrterm -> Glob_term.glob_constr val pf_intern_term : - Tacinterp.interp_sign -> Proof_type.goal Evd.sigma -> + Tacinterp.interp_sign -> Goal.goal Evd.sigma -> ssrterm -> Glob_term.glob_constr val interp_term : - Tacinterp.interp_sign -> Proof_type.goal Evd.sigma -> + Tacinterp.interp_sign -> Goal.goal Evd.sigma -> ssrterm -> evar_map * EConstr.t val interp_wit : @@ -136,28 +136,28 @@ val interp_hyp : ist -> goal sigma -> ssrhyp -> evar_map * ssrhyp val interp_hyps : ist -> goal sigma -> ssrhyps -> evar_map * ssrhyps val interp_refine : - Tacinterp.interp_sign -> Proof_type.goal Evd.sigma -> + Tacinterp.interp_sign -> Goal.goal Evd.sigma -> Glob_term.glob_constr -> evar_map * (evar_map * EConstr.constr) val interp_open_constr : - Tacinterp.interp_sign -> Proof_type.goal Evd.sigma -> + Tacinterp.interp_sign -> Goal.goal Evd.sigma -> Tacexpr.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) val pf_e_type_of : - Proof_type.goal Evd.sigma -> - EConstr.constr -> Proof_type.goal Evd.sigma * EConstr.types + Goal.goal Evd.sigma -> + EConstr.constr -> Goal.goal Evd.sigma * EConstr.types val splay_open_constr : - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> evar_map * EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t -val isAppInd : Proof_type.goal Evd.sigma -> EConstr.types -> bool +val isAppInd : Goal.goal Evd.sigma -> EConstr.types -> bool val interp_view_nbimps : Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> Glob_term.glob_constr -> int + Goal.goal Evd.sigma -> Glob_term.glob_constr -> int val interp_nbargs : Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> Glob_term.glob_constr -> int + Goal.goal Evd.sigma -> Glob_term.glob_constr -> int val mk_term : ssrtermkind -> 'b -> ssrtermkind * (Glob_term.glob_constr * 'b option) @@ -169,20 +169,20 @@ val mk_internal_id : string -> Id.t val mk_tagged_id : string -> int -> Id.t val mk_evar_name : int -> Name.t val ssr_anon_hyp : string -val pf_type_id : Proof_type.goal Evd.sigma -> EConstr.types -> Id.t +val pf_type_id : Goal.goal Evd.sigma -> EConstr.types -> Id.t val pf_abs_evars : - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> evar_map * EConstr.t -> int * EConstr.t * Evar.t list * UState.t val pf_abs_evars2 : (* ssr2 *) - Proof_type.goal Evd.sigma -> Evar.t list -> + Goal.goal Evd.sigma -> Evar.t list -> evar_map * EConstr.t -> int * EConstr.t * Evar.t list * UState.t val pf_abs_cterm : - Proof_type.goal Evd.sigma -> int -> EConstr.t -> EConstr.t + Goal.goal Evd.sigma -> int -> EConstr.t -> EConstr.t val pf_merge_uc : UState.t -> 'a Evd.sigma -> 'a Evd.sigma @@ -190,21 +190,21 @@ val pf_merge_uc_of : evar_map -> 'a Evd.sigma -> 'a Evd.sigma val constr_name : evar_map -> EConstr.t -> Name.t val pf_type_of : - Proof_type.goal Evd.sigma -> - Term.constr -> Proof_type.goal Evd.sigma * Term.types + Goal.goal Evd.sigma -> + Term.constr -> Goal.goal Evd.sigma * Term.types val pfe_type_of : - Proof_type.goal Evd.sigma -> - EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types + Goal.goal Evd.sigma -> + EConstr.t -> Goal.goal Evd.sigma * EConstr.types val pf_abs_prod : Name.t -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> EConstr.t -> - EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types + EConstr.t -> Goal.goal Evd.sigma * EConstr.types val pf_mkprod : - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> EConstr.t -> ?name:Name.t -> - EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types + EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option val mkSsrRef : string -> Globnames.global_reference @@ -213,15 +213,15 @@ val mkSsrConst : env -> evar_map -> evar_map * EConstr.t val pf_mkSsrConst : string -> - Proof_type.goal Evd.sigma -> - EConstr.t * Proof_type.goal Evd.sigma + Goal.goal Evd.sigma -> + EConstr.t * Goal.goal Evd.sigma val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : Globnames.global_reference -> - Proof_type.goal Evd.sigma -> - Term.constr * Proof_type.goal Evd.sigma + Goal.goal Evd.sigma -> + Term.constr * Goal.goal Evd.sigma val is_discharged_id : Id.t -> bool val mk_discharged_id : Id.t -> Id.t @@ -230,15 +230,15 @@ val has_discharged_tag : string -> bool val ssrqid : string -> Libnames.qualid val new_tmp_id : tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx -val mk_anon_id : string -> Proof_type.goal Evd.sigma -> Id.t +val mk_anon_id : string -> Goal.goal Evd.sigma -> Id.t val pf_abs_evars_pirrel : - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> evar_map * Term.constr -> int * Term.constr -val pf_nbargs : Proof_type.goal Evd.sigma -> EConstr.t -> int +val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int val gen_tmp_ids : ?ist:Geninterp.interp_sign -> - (Proof_type.goal * tac_ctx) Evd.sigma -> - (Proof_type.goal * tac_ctx) list Evd.sigma + (Goal.goal * tac_ctx) Evd.sigma -> + (Goal.goal * tac_ctx) list Evd.sigma val ssrevaltac : Tacinterp.interp_sign -> Tacinterp.Value.t -> Proofview.V82.tac @@ -258,23 +258,23 @@ val ssrautoprop_tac : val mkProt : EConstr.t -> EConstr.t -> - Proof_type.goal Evd.sigma -> - EConstr.t * Proof_type.goal Evd.sigma + Goal.goal Evd.sigma -> + EConstr.t * Goal.goal Evd.sigma val mkEtaApp : EConstr.t -> int -> int -> EConstr.t val mkRefl : EConstr.t -> EConstr.t -> - Proof_type.goal Evd.sigma -> EConstr.t * Proof_type.goal Evd.sigma + Goal.goal Evd.sigma -> EConstr.t * Goal.goal Evd.sigma val discharge_hyp : Id.t * (Id.t * string) -> - Proof_type.goal Evd.sigma -> Evar.t list Evd.sigma + Goal.goal Evd.sigma -> Evar.t list Evd.sigma val clear_wilds_and_tmp_and_delayed_ids : - (Proof_type.goal * tac_ctx) Evd.sigma -> - (Proof_type.goal * tac_ctx) list Evd.sigma + (Goal.goal * tac_ctx) Evd.sigma -> + (Goal.goal * tac_ctx) list Evd.sigma val view_error : string -> ssrterm -> 'a @@ -284,14 +284,14 @@ val top_id : Id.t val pf_abs_ssrterm : ?resolve_typeclasses:bool -> ist -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> ssrterm -> evar_map * EConstr.t * UState.t * int val pf_interp_ty : ?resolve_typeclasses:bool -> Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) -> int * EConstr.t * EConstr.t * UState.t @@ -309,12 +309,12 @@ exception NotEnoughProducts val pf_saturate : ?beta:bool -> ?bi_types:bool -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> EConstr.constr -> ?ty:EConstr.types -> int -> EConstr.constr * EConstr.types * (int * EConstr.constr) list * - Proof_type.goal Evd.sigma + Goal.goal Evd.sigma val saturate : ?beta:bool -> ?bi_types:bool -> @@ -338,32 +338,32 @@ type name_hint = (int * EConstr.types array) option ref val gentac : (Geninterp.interp_sign -> (Ssrast.ssrdocc) * - Ssrmatching_plugin.Ssrmatching.cpattern -> Proof_type.tactic) + Ssrmatching_plugin.Ssrmatching.cpattern -> Tacmach.tactic) val genstac : ((Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern) list * Ssrast.ssrhyp list -> - Tacinterp.interp_sign -> Proof_type.tactic + Tacinterp.interp_sign -> Tacmach.tactic val pf_interp_gen : Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> bool -> (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern -> EConstr.t * EConstr.t * Ssrast.ssrhyp list * - Proof_type.goal Evd.sigma + Goal.goal Evd.sigma val pf_interp_gen_aux : Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> bool -> (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern -> bool * Ssrmatching_plugin.Ssrmatching.pattern * EConstr.t * EConstr.t * Ssrast.ssrhyp list * UState.t * - Proof_type.goal Evd.sigma + Goal.goal Evd.sigma val is_name_in_ipats : Id.t -> ssripats -> bool @@ -386,12 +386,12 @@ val interp_clr : val genclrtac : EConstr.constr -> - EConstr.constr list -> Ssrast.ssrhyp list -> Proof_type.tactic + EConstr.constr list -> Ssrast.ssrhyp list -> Tacmach.tactic val cleartac : ssrhyps -> v82tac -val tclMULT : int * ssrmmod -> Proof_type.tactic -> Proof_type.tactic +val tclMULT : int * ssrmmod -> Tacmach.tactic -> Tacmach.tactic -val unprotecttac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma +val unprotecttac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val abs_wgen : bool -> @@ -401,8 +401,8 @@ val abs_wgen : ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option -> - Proof_type.goal Evd.sigma * EConstr.t list * EConstr.t -> - Proof_type.goal Evd.sigma * EConstr.t list * EConstr.t + Goal.goal Evd.sigma * EConstr.t list * EConstr.t -> + Goal.goal Evd.sigma * EConstr.t list * EConstr.t val clr_of_wgen : ssrhyps * ((ssrhyp_or_id * 'a) * 'b option) option -> diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index 8dc28d8b7..825b4758e 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -32,23 +32,23 @@ val ssrelim : (?ist:Ltac_plugin.Tacinterp.interp_sign -> 'a -> Ssrast.ssripat option -> - (Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma) -> - bool -> Ssrast.ssrhyp list -> Proof_type.tactic) -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + (Goal.goal Evd.sigma -> Goal.goal list Evd.sigma) -> + bool -> Ssrast.ssrhyp list -> Tacmach.tactic) -> + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val elimtac : EConstr.constr -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val casetac : EConstr.constr -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val is_injection_case : EConstr.t -> Proof_type.goal Evd.sigma -> bool +val is_injection_case : EConstr.t -> Goal.goal Evd.sigma -> bool val perform_injection : EConstr.constr -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val ssrscasetac : bool -> EConstr.constr -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index f712002c1..f9ab5d74f 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -25,12 +25,12 @@ val mkclr : ssrclear -> ssrdocc val nodocc : ssrdocc val noclr : ssrdocc -val simpltac : Ssrast.ssrsimpl -> Proof_type.tactic +val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic val newssrcongrtac : int * Ssrast.ssrterm -> Ltac_plugin.Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val mk_rwarg : @@ -45,7 +45,7 @@ val ssrinstancesofrule : Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrdir -> Ssrast.ssrterm -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val ssrrewritetac : Ltac_plugin.Tacinterp.interp_sign -> @@ -53,11 +53,11 @@ val ssrrewritetac : (((Ssrast.ssrhyps option * Ssrmatching.occ) * Ssrmatching.rpattern option) * (ssrwkind * Ssrast.ssrterm))) - list -> Proof_type.tactic + list -> Tacmach.tactic -val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Proof_type.tactic +val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic val unlocktac : Ltac_plugin.Tacinterp.interp_sign -> (Ssrmatching.occ * Ssrast.ssrterm) list -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index ead361745..7f254074c 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -36,7 +36,7 @@ val ssrabstract : val basecuttac : string -> - EConstr.t -> Proof_type.goal Evd.sigma -> Evar.t list Evd.sigma + EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma val wlogtac : Ltac_plugin.Tacinterp.interp_sign -> @@ -52,7 +52,7 @@ val wlogtac : Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> bool -> [< `Gen of Names.Id.t option option | `NoGen > `NoGen ] -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val sufftac : Ssrast.ist -> @@ -62,5 +62,5 @@ val sufftac : (Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option))) * (bool * Tacinterp.Value.t option list)) -> - Proof_type.tactic + Tacmach.tactic diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 7ae9e3824..06bbd749e 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -175,10 +175,10 @@ let move_top_with_view ~next c r v = type block_names = (int * EConstr.types array) option -let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Proof_type.tactic), +let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic), (tclEQINTROS : ?ind:block_names ref -> ?ist:Tacinterp.interp_sign -> - Proof_type.tactic -> Proof_type.tactic -> ssripats -> - Proof_type.tactic) + Tacmach.tactic -> Tacmach.tactic -> ssripats -> + Tacmach.tactic) = let rec ipattac ?ist ~next p : tac_ctx tac_a = fun gl -> diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index 5f5c7f34a..aefdc8e11 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -36,10 +36,10 @@ val elim_intro_tac : ?ist:Tacinterp.interp_sign -> [> `EConstr of 'a * 'b * EConstr.t ] -> Ssrast.ssripat option -> - Proof_type.tactic -> + Tacmach.tactic -> bool -> Ssrast.ssrhyp list -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma (* "move=> top; tac top; clear top" respecting the speed *) val with_top : (EConstr.t -> v82tac) -> tac_ctx tac_a @@ -51,17 +51,17 @@ val ssrmovetac : (((Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear) * Ssrast.ssripats)) -> - Proof_type.tactic + Tacmach.tactic -val movehnftac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma +val movehnftac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val with_dgens : (Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear -> ((Ssrast.ssrdocc * Ssrmatching.cpattern) list -> Ssrast.ssrdocc * Ssrmatching.cpattern -> - Ltac_plugin.Tacinterp.interp_sign -> Proof_type.tactic) -> - Ltac_plugin.Tacinterp.interp_sign -> Proof_type.tactic + Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic) -> + Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic val ssrcasetac : Ltac_plugin.Tacinterp.interp_sign -> @@ -69,7 +69,7 @@ val ssrcasetac : (Ssrast.ssripat option * (((Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear) * Ssrast.ssripats)) -> - Proof_type.tactic + Tacmach.tactic val ssrapplytac : Tacinterp.interp_sign -> @@ -79,5 +79,5 @@ val ssrapplytac : (Ssrast.ssrtermkind * Tacexpr.glob_constr_and_expr)) list list * Ssrast.ssrhyps) * Ssrast.ssripats)) -> - Proof_type.tactic + Tacmach.tactic diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 9207b9e43..8da9bc72b 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -12,7 +12,7 @@ open API open Ssrast val pp_term : - Proof_type.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds + Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds val pr_spc : unit -> Pp.std_ppcmds val pr_bar : unit -> Pp.std_ppcmds diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index 1d1887138..297cfdfdc 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -17,7 +17,7 @@ val tclSEQAT : int Misctypes.or_var * (('a * Ltac_plugin.Tacinterp.Value.t option list) * Ltac_plugin.Tacinterp.Value.t option) -> - Proof_type.tactic + Tacmach.tactic val tclCLAUSES : Ltac_plugin.Tacinterp.interp_sign -> @@ -27,7 +27,7 @@ val tclCLAUSES : Ssrmatching_plugin.Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val hinttac : Tacinterp.interp_sign -> @@ -42,5 +42,5 @@ val ssrdotac : Ssrmatching_plugin.Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq) -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 91e40f368..cc142e091 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -80,7 +80,7 @@ let interp_view ist si env sigma gv v rid = snd (view_with (if view_nbimps < 0 then [] else viewtab.(0))) -let with_view ist ~next si env (gl0 : (Proof_type.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr = +let with_view ist ~next si env (gl0 : (Goal.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr = let c2r ist x = { ist with lfun = Id.Map.add top_id (Value.of_constr x) ist.lfun } in let terminate (sigma, c') = -- cgit v1.2.3