aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrast.mli8
-rw-r--r--plugins/ssr/ssrcommon.ml40
-rw-r--r--plugins/ssr/ssrcommon.mli22
-rw-r--r--plugins/ssr/ssrequality.ml4
-rw-r--r--plugins/ssr/ssrfwd.ml2
-rw-r--r--plugins/ssr/ssripats.ml6
-rw-r--r--plugins/ssr/ssrparser.ml46
-rw-r--r--plugins/ssr/ssrtacticals.ml7
-rw-r--r--plugins/ssr/ssrvernac.ml42
9 files changed, 48 insertions, 49 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 4ddd38365..0f4b86d10 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -94,10 +94,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 *)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 38ee4be45..d389f7085 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -13,7 +13,7 @@ open Grammar_API
open Util
open Names
open Evd
-open Constr
+open Term
open Termops
open Printer
open Locusops
@@ -133,7 +133,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;
}
@@ -308,7 +308,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 +318,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 +327,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 +341,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 +357,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 +385,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 +403,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 +602,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 +626,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 +691,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 +703,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 +814,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"
@@ -1082,7 +1082,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 1b6a700b2..7a4b47a46 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -57,7 +57,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;
@@ -175,17 +175,17 @@ val pf_abs_evars :
Proof_type.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 ->
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
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
@@ -196,14 +196,14 @@ val pfe_type_of :
Proof_type.goal Evd.sigma ->
EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types
val pf_abs_prod :
- Names.name ->
+ Name.t ->
Proof_type.goal Evd.sigma ->
EConstr.t ->
EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types
val pf_mkprod :
Proof_type.goal Evd.sigma ->
EConstr.t ->
- ?name:Names.name ->
+ ?name:Name.t ->
EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types
val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
@@ -229,7 +229,7 @@ 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
+ tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx
val mk_anon_id : string -> Proof_type.goal Evd.sigma -> Id.t
val pf_abs_evars_pirrel :
Proof_type.goal Evd.sigma ->
@@ -286,7 +286,7 @@ val pf_abs_ssrterm :
ist ->
Proof_type.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 ->
@@ -294,7 +294,7 @@ val pf_interp_ty :
Proof_type.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
@@ -362,7 +362,7 @@ val pf_interp_gen_aux :
(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 *
+ EConstr.t * Ssrast.ssrhyp list * UState.t *
Proof_type.goal Evd.sigma
val is_name_in_ipats :
@@ -377,7 +377,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
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index dbe13aec9..b0fe89897 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -343,9 +343,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/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 2b10f2f35..660c2e776 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -201,7 +201,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/ssripats.ml b/plugins/ssr/ssripats.ml
index 96a75ba27..4a9dddd2b 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -117,7 +117,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 +133,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 +143,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
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 5fd377233..3ea8c2431 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -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/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 67b705190..b586d05e1 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -10,7 +10,6 @@
open API
open Names
-open Constr
open Termops
open Tacmach
open Misctypes
@@ -103,10 +102,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/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 6fbfbf03c..4c8827bf8 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -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 _ ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 04:49:00 +0000