diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrast.mli | 13 | ||||
| -rw-r--r-- | plugins/ssr/ssrbwd.ml | 1 | ||||
| -rw-r--r-- | plugins/ssr/ssrbwd.mli | 5 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 47 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 129 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 1 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.mli | 17 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 5 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.mli | 13 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.mli | 7 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 15 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.mli | 17 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 10 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mli | 1 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.ml | 1 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.mli | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.mli | 7 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.ml | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.mli | 1 |
22 files changed, 146 insertions, 167 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 4ddd383654..cdd4ee6459 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Ltac_plugin @@ -94,10 +93,10 @@ type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats type ssrfwdid = Id.t (** Binders (for fwd tactics) *) type 'term ssrbind = - | Bvar of name - | Bdecl of name list * 'term - | Bdef of name * 'term option * 'term - | Bstruct of name + | Bvar of Name.t + | Bdecl of Name.t list * 'term + | Bdef of Name.t * 'term option * 'term + | Bstruct of Name.t | Bcast of 'term (* We use an intermediate structure to correctly render the binder list *) (* abbreviations. We use a list of hints to extract the binders and *) @@ -145,6 +144,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.ml b/plugins/ssr/ssrbwd.ml index 3988f00bad..cc0e86684e 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Printer open Pretyping open Globnames diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index b0e98bdb47..af9f7491ad 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -8,9 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -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 +18,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 38ee4be45d..608b778e4f 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -8,12 +8,11 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API open Util open Names open Evd -open Constr +open Term open Termops open Printer open Locusops @@ -133,7 +132,7 @@ let tac_on_all gl tac = (* Used to thread data between intro patterns at run time *) type tac_ctx = { - tmp_ids : (Id.t * name ref) list; + tmp_ids : (Id.t * Name.t ref) list; wild_ids : Id.t list; delayed_clears : Id.t list; } @@ -226,8 +225,8 @@ let isAppInd gl c = let interp_refine ist gl rc = let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in - let vars = { Pretyping.empty_lvar with - Pretyping.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun + let vars = { Glob_ops.empty_lvar with + Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { @@ -308,7 +307,7 @@ let is_internal_name s = List.exists (fun p -> p s) !internal_names let tmp_tag = "_the_" let tmp_post = "_tmp_" let mk_tmp_id i = - id_of_string (Printf.sprintf "%s%s%s" tmp_tag (CString.ordinal i) tmp_post) + Id.of_string (Printf.sprintf "%s%s%s" tmp_tag (CString.ordinal i) tmp_post) let new_tmp_id ctx = let id = mk_tmp_id (1 + List.length ctx.tmp_ids) in let orig = ref Anonymous in @@ -318,7 +317,7 @@ let new_tmp_id ctx = let mk_internal_id s = let s' = Printf.sprintf "_%s_" s in let s' = String.map (fun c -> if c = ' ' then '_' else c) s' in - add_internal_name ((=) s'); id_of_string s' + add_internal_name ((=) s'); Id.of_string s' let same_prefix s t n = let rec loop i = i = n || s.[i] = t.[i] && loop (i + 1) in loop 0 @@ -327,7 +326,7 @@ let skip_digits s = let n = String.length s in let rec loop i = if i < n && is_digit s.[i] then loop (i + 1) else i in loop -let mk_tagged_id t i = id_of_string (Printf.sprintf "%s%d_" t i) +let mk_tagged_id t i = Id.of_string (Printf.sprintf "%s%d_" t i) let is_tagged t s = let n = String.length s - 1 and m = String.length t in m < n && s.[n] = '_' && same_prefix s t m && skip_digits s m = n @@ -341,7 +340,7 @@ let ssr_anon_hyp = "Hyp" let wildcard_tag = "_the_" let wildcard_post = "_wildcard_" let mk_wildcard_id i = - id_of_string (Printf.sprintf "%s%s%s" wildcard_tag (CString.ordinal i) wildcard_post) + Id.of_string (Printf.sprintf "%s%s%s" wildcard_tag (CString.ordinal i) wildcard_post) let has_wildcard_tag s = let n = String.length s in let m = String.length wildcard_tag in let m' = String.length wildcard_post in @@ -357,15 +356,15 @@ let new_wild_id ctx = let discharged_tag = "_discharged_" let mk_discharged_id id = - id_of_string (Printf.sprintf "%s%s_" discharged_tag (string_of_id id)) + Id.of_string (Printf.sprintf "%s%s_" discharged_tag (Id.to_string id)) let has_discharged_tag s = let m = String.length discharged_tag and n = String.length s - 1 in m < n && s.[n] = '_' && same_prefix s discharged_tag m let _ = add_internal_name has_discharged_tag -let is_discharged_id id = has_discharged_tag (string_of_id id) +let is_discharged_id id = has_discharged_tag (Id.to_string id) let max_suffix m (t, j0 as tj0) id = - let s = string_of_id id in let n = String.length s - 1 in + let s = Id.to_string id in let n = String.length s - 1 in let dn = String.length t - 1 - n in let i0 = j0 - dn in if not (i0 >= m && s.[n] = '_' && same_prefix s t m) then tj0 else let rec loop i = @@ -385,7 +384,7 @@ let mk_anon_id t gl = let rec loop i j = let d = !s.[i] in if not (is_digit d) then i + 1, j else loop (i - 1) (if d = '0' then j else i) in - let m, j = loop (n - 1) n in m, (!s, j), id_of_string !s in + let m, j = loop (n - 1) n in m, (!s, j), Id.of_string !s in let gl_ids = pf_ids_of_hyps gl in if not (List.mem id0 gl_ids) then id0 else let s, i = List.fold_left (max_suffix m) si0 gl_ids in @@ -403,7 +402,7 @@ let convert_concl t = Tactics.convert_concl t Term.DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with - | Constr.Prod(_,src,tgt) -> + | Term.Prod(_,src,tgt) -> Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl | _ -> CErrors.anomaly (str "gentac creates no product") @@ -602,7 +601,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let rec loopP evlist c i = function | (_, (n, t, _)) :: evl -> let t = get evlist (i - 1) t in - let n = Name (id_of_string (ssr_anon_hyp ^ string_of_int n)) in + let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in loopP evlist (mkProd (n, t, c)) (i - 1) evl | [] -> c in let rec loop c i = function @@ -626,13 +625,13 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let nb_evar_deps = function | Name id -> - let s = string_of_id id in + let s = Id.to_string id in if not (is_tagged evar_tag s) then 0 else let m = String.length evar_tag in (try int_of_string (String.sub s m (String.length s - 1 - m)) with _ -> 0) | _ -> 0 -let pf_type_id gl t = id_of_string (Namegen.hdchar (pf_env gl) (project gl) t) +let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t) let pfe_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty @@ -691,7 +690,7 @@ let pf_merge_uc_of sigma gl = let rec constr_name sigma c = match EConstr.kind sigma c with | Var id -> Name id | Cast (c', _, _) -> constr_name sigma c' - | Const (cn,_) -> Name (Label.to_id (con_label cn)) + | Const (cn,_) -> Name (Label.to_id (Constant.label cn)) | App (c', _) -> constr_name sigma c' | _ -> Anonymous @@ -703,9 +702,9 @@ let pf_mkprod gl c ?(name=constr_name (project gl) c) cl = let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project gl) c cl) (** look up a name in the ssreflect internals module *) -let ssrdirpath = DirPath.make [id_of_string "ssreflect"] -let ssrqid name = Libnames.make_qualid ssrdirpath (id_of_string name) -let ssrtopqid name = Libnames.qualid_of_ident (id_of_string name) +let ssrdirpath = DirPath.make [Id.of_string "ssreflect"] +let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) +let ssrtopqid name = Libnames.qualid_of_ident (Id.of_string name) let locate_reference qid = Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let mkSsrRef name = @@ -814,7 +813,7 @@ let ssr_n_tac seed n gl = let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in let fail msg = CErrors.user_err (Pp.str msg) in let tacname = - try Nametab.locate_tactic (Libnames.qualid_of_ident (id_of_string name)) + try Nametab.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) with Not_found -> try Nametab.locate_tactic (ssrqid name) with Not_found -> if n = -1 then fail "The ssreflect library was not loaded" @@ -960,7 +959,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)); - Refiner.refiner (Proof_type.Refine (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 @@ -1082,7 +1081,7 @@ let introid ?(orig=ref Anonymous) name = tclTHEN (fun gl -> let anontac decl gl = let id = match RelDecl.get_name decl with | Name id -> - if is_discharged_id id then id else mk_anon_id (string_of_id id) gl + if is_discharged_id id then id else mk_anon_id (Id.to_string id) gl | _ -> mk_anon_id ssr_anon_hyp gl in introid id gl diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 1b6a700b2d..4b045e989a 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -8,10 +8,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 @@ -57,7 +56,7 @@ type 'a tac_a = (goal * 'a) sigma -> (goal * 'a) list sigma (* Thread around names to be cleared or generalized back, and the speed *) type tac_ctx = { - tmp_ids : (Id.t * name ref) list; + tmp_ids : (Id.t * Name.t ref) list; wild_ids : Id.t list; (* List of variables to be cleared at the end of the sentence *) delayed_clears : Id.t list; @@ -122,11 +121,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 +135,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,42 +168,42 @@ 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 * - Evd.evar_universe_context + 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 * - Evd.evar_universe_context + 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 : - Evd.evar_universe_context -> 'a Evd.sigma -> 'a Evd.sigma + UState.t -> 'a Evd.sigma -> 'a Evd.sigma 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 : - Names.name -> - Proof_type.goal Evd.sigma -> + Name.t -> + 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:Names.name -> - EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types + ?name:Name.t -> + 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 +212,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 @@ -229,16 +228,16 @@ val is_tagged : string -> string -> bool val has_discharged_tag : string -> bool val ssrqid : string -> Libnames.qualid val new_tmp_id : - tac_ctx -> (Names.Id.t * Names.name ref) * tac_ctx -val mk_anon_id : string -> Proof_type.goal Evd.sigma -> Id.t + tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx +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 +257,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,17 +283,17 @@ 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 * Evd.evar_universe_context * int + 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 * Evd.evar_universe_context + int * EConstr.t * EConstr.t * UState.t val ssr_n_tac : string -> int -> v82tac val donetac : int -> v82tac @@ -309,12 +308,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 +337,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 * Evd.evar_universe_context * - Proof_type.goal Evd.sigma + EConstr.t * Ssrast.ssrhyp list * UState.t * + Goal.goal Evd.sigma val is_name_in_ipats : Id.t -> ssripats -> bool @@ -377,7 +376,7 @@ val mk_profiler : string -> profiler (** Basic tactics *) -val introid : ?orig:name ref -> Id.t -> v82tac +val introid : ?orig:Name.t ref -> Id.t -> v82tac val intro_anon : v82tac val intro_all : v82tac @@ -386,12 +385,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 +400,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.ml b/plugins/ssr/ssrelim.ml index bd9a05891a..832044909c 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Util open Names open Printer diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index 8dc28d8b75..66e202b48f 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin val ssrelim : @@ -32,23 +31,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.ml b/plugins/ssr/ssrequality.ml index dbe13aec9f..ab6a60f4ee 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ltac_plugin open Util open Names @@ -343,9 +342,9 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = Term.destConst elim in - let mp,dp,l = repr_con (constant_of_kn (canonical_con elim)) in + let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (canonical_con (make_con mp dp l')) in + let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in mkConst c1', gl in let elim = EConstr.of_constr elim in let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index f712002c1f..a3366887fb 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin open Ssrast @@ -25,12 +24,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 +44,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 +52,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.ml b/plugins/ssr/ssrfwd.ml index 2b10f2f35b..8e6329a15e 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Tacmach @@ -201,7 +200,7 @@ let havetac ist let assert_is_conv gl = try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ - pr_econstr (EConstr.mkArrow (EConstr.mkVar (id_of_string "_")) concl)) in + pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index ead361745d..e5b5b58fff 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Ltac_plugin @@ -36,7 +35,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 +51,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 +61,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 96a75ba27f..023778fdbf 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Pp open Term @@ -95,7 +94,7 @@ let ssrmkabs id gl = end in Proofview.V82.of_tactic (Proofview.tclTHEN - (Tactics.New.refine step) + (Tactics.New.refine ~typecheck:false step) (Proofview.tclFOCUS 1 3 Proofview.shelve)) gl let ssrmkabstac ids = @@ -117,7 +116,7 @@ let delayed_clear force rest clr gl = let ren_clr, ren = List.split (List.map (fun x -> let x = hyp_id x in - let x' = mk_anon_id (string_of_id x) gl in + let x' = mk_anon_id (Id.to_string x) gl in x', (x, x')) clr) in let ctx = { ctx with delayed_clears = ren_clr @ ctx.delayed_clears } in let gl = push_ctx ctx gl in @@ -133,7 +132,7 @@ let with_defective maintac deps clr ist gl = let top_id = match EConstr.kind_of_type (project gl) (pf_concl gl) with | ProdType (Name id, _, _) - when has_discharged_tag (string_of_id id) -> id + when has_discharged_tag (Id.to_string id) -> id | _ -> top_id in let top_gen = mkclr clr, cpattern_of_id top_id in tclTHEN (introid top_id) (maintac deps top_gen ist) gl @@ -143,7 +142,7 @@ let with_defective_a maintac deps clr ist gl = let top_id = match EConstr.kind_of_type sigma (without_ctx pf_concl gl) with | ProdType (Name id, _, _) - when has_discharged_tag (string_of_id id) -> id + when has_discharged_tag (Id.to_string id) -> id | _ -> top_id in let top_gen = mkclr clr, cpattern_of_id top_id in tclTHEN_a (tac_ctx (introid top_id)) (maintac deps top_gen ist) gl @@ -175,10 +174,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 5f5c7f34a4..6c36e67e83 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin open Ssrast open Ssrcommon @@ -36,10 +35,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 +50,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 +68,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 +78,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/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 5fd3772338..228444b82e 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API open Names open Pp @@ -346,7 +345,8 @@ let interp_index ist gl idx = | Some c -> let rc = Detyping.detype false [] (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with - | _, Constrexpr.Numeral bigi -> int_of_string (Bigint.to_string bigi) + | _, Constrexpr.Numeral (s,b) -> + let n = int_of_string s in if b then n else -n | _ -> raise Not_found end | None -> raise Not_found @@ -1465,7 +1465,7 @@ let ssr_id_of_string loc s = else Feedback.msg_warning (str ( "The name " ^ s ^ " fits the _xxx_ format used for anonymous variables.\n" ^ "Scripts with explicit references to anonymous variables are fragile.")) - end; id_of_string s + end; Id.of_string s let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ()) @@ -1555,7 +1555,7 @@ END let ssrautoprop gl = try let tacname = - try Nametab.locate_tactic (qualid_of_ident (id_of_string "ssrautoprop")) + try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl @@ -2320,7 +2320,7 @@ let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma GEXTEND Gram GLOBAL: ssr_idcomma; ssr_idcomma: [ [ test_idcomma; - ip = [ id = IDENT -> Some (id_of_string id) | "_" -> None ]; "," -> + ip = [ id = IDENT -> Some (Id.of_string id) | "_" -> None ]; "," -> Some ip ] ]; END diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 1548206666..c93e104056 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 427109c1b2..e865ef706d 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Pp open Names open Printer diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 9207b9e437..5c68872b75 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -8,11 +8,10 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -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.ml b/plugins/ssr/ssrtacticals.ml index 67b7051902..5e43c83749 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -8,9 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names -open Constr open Termops open Tacmach open Misctypes @@ -103,10 +101,10 @@ let endclausestac id_map clseq gl_id cl0 gl = | ids, dc' -> forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in let rec unmark c = match EConstr.kind (project gl) c with - | Var id when hidden_clseq clseq && id = gl_id -> cl0 - | Prod (Name id, t, c') when List.mem_assoc id id_map -> + | Term.Var id when hidden_clseq clseq && id = gl_id -> cl0 + | Term.Prod (Name id, t, c') when List.mem_assoc id id_map -> EConstr.mkProd (Name (orig_id id), unmark t, unmark c') - | LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> + | Term.LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c') | _ -> EConstr.map (project gl) unmark c in let utac hyp = diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index 1d18871387..c1f65a31e9 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API val tclSEQAT : Ltac_plugin.Tacinterp.interp_sign -> @@ -17,7 +16,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 +26,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 +41,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/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 6fbfbf03c7..fbe3cd2b91 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API open Names open Term @@ -337,7 +336,8 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - Reductionops.splay_prod env sigma (EConstr.of_constr (Universes.unsafe_type_of_global hr)) in + let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in + Reductionops.splay_prod env sigma (EConstr.of_constr hr) in let np = List.length dc in if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in @@ -355,7 +355,7 @@ let coerce_search_pattern_to_sort hpat = let coerce hp coe_index = let coe = Classops.get_coercion_value coe_index in try - let coe_ref = reference_of_constr coe in + let coe_ref = global_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with _ -> diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 91e40f3684..338ecccc2d 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Util open Names open Term @@ -80,7 +79,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') = diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index 8a7bd5d6e7..6fd906ff4f 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrast open Ssrcommon |