aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml37
-rw-r--r--plugins/ssr/ssrcommon.mli4
-rw-r--r--plugins/ssr/ssrelim.ml5
-rw-r--r--plugins/ssr/ssrequality.ml30
-rw-r--r--plugins/ssr/ssrfwd.ml4
-rw-r--r--plugins/ssr/ssripats.ml42
-rw-r--r--plugins/ssr/ssrparser.ml46
-rw-r--r--plugins/ssr/ssrparser.mli4
-rw-r--r--plugins/ssr/ssrtacticals.ml12
-rw-r--r--plugins/ssr/ssrvernac.ml47
-rw-r--r--plugins/ssr/ssrview.ml6
11 files changed, 86 insertions, 71 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d5118da4cb..3f6503e73c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -423,12 +423,12 @@ let mk_anon_id t gl_ids =
(set s i (Char.chr (Char.code (get s i) + 1)); s) in
Id.of_bytes (loop (n - 1))
-let convert_concl_no_check t = Tactics.convert_concl_no_check t Term.DEFAULTcast
-let convert_concl t = Tactics.convert_concl t Term.DEFAULTcast
+let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast
+let convert_concl t = Tactics.convert_concl t DEFAULTcast
let rename_hd_prod orig_name_ref gl =
match EConstr.kind (project gl) (pf_concl gl) with
- | Term.Prod(_,src,tgt) ->
+ | 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")
@@ -504,16 +504,17 @@ let nf_evar sigma t =
EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
let pf_abs_evars2 gl rigid (sigma, c0) =
- let c0 = EConstr.to_constr sigma c0 in
+ let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in
let sigma0, ucst = project gl, Evd.evar_universe_context sigma in
let nenv = env_size (pf_env gl) in
let abs_evar n k =
let evi = Evd.find sigma k in
- let dc = CList.firstn n (evar_filtered_context evi) in
+ let concl = EConstr.Unsafe.to_constr evi.evar_concl in
+ let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in
let abs_dc c = function
| NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c)
| NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in
- let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in
+ let t = Context.Named.fold_inside abs_dc ~init:concl dc in
nf_evar sigma t in
let rec put evlist c = match Constr.kind c with
| Evar (k, a) ->
@@ -569,11 +570,12 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
let nenv = env_size (pf_env gl) in
let abs_evar n k =
let evi = Evd.find sigma k in
- let dc = CList.firstn n (evar_filtered_context evi) in
+ let concl = EConstr.Unsafe.to_constr evi.evar_concl in
+ let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in
let abs_dc c = function
| NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c)
| NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in
- let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in
+ let t = Context.Named.fold_inside abs_dc ~init:concl dc in
nf_evar sigma0 (nf_evar sigma t) in
let rec put evlist c = match Constr.kind c with
| Evar (k, a) ->
@@ -581,7 +583,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
let n = max 0 (Array.length a - nenv) in
let k_ty =
Retyping.get_sort_family_of
- (pf_env gl) sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))) in
+ (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in
let is_prop = k_ty = InProp in
let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t
| _ -> Constr.fold put evlist c in
@@ -746,7 +748,7 @@ let pf_mkSsrConst name gl =
let pf_fresh_global name gl =
let sigma, env, it = project gl, pf_env gl, sig_it gl in
let sigma,t = Evd.fresh_global env sigma name in
- t, re_sig it sigma
+ EConstr.Unsafe.to_constr t, re_sig it sigma
let mkProt t c gl =
let prot, gl = pf_mkSsrConst "protect_term" gl in
@@ -800,8 +802,11 @@ let rec is_name_in_ipats name = function
List.exists (function SsrHyp(_,id) -> id = name) clr
|| is_name_in_ipats name tl
| IPatId id :: tl -> id = name || is_name_in_ipats name tl
- | (IPatCase l | IPatDispatch l) :: tl -> List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl
- | _ :: tl -> is_name_in_ipats name tl
+ | IPatAbstractVars ids :: tl ->
+ CList.mem_f Id.equal name ids || is_name_in_ipats name tl
+ | (IPatCase l | IPatDispatch l | IPatInj l) :: tl ->
+ List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl
+ | (IPatView _ | IPatAnon _ | IPatSimpl _ | IPatRewrite _ | IPatTac _ | IPatNoop) :: tl -> is_name_in_ipats name tl
| [] -> false
let view_error s gv =
@@ -980,7 +985,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
if not (EConstr.Vars.closed0 sigma ty) then
raise dependent_apply_error;
let m = Evarutil.new_meta () in
- loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1)
+ loop (meta_declare m ty sigma) bo ((EConstr.mkMeta m)::args) (n-1)
| _ -> assert false
in loop sigma t [] n in
pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
@@ -1216,7 +1221,7 @@ let genclrtac cl cs clr =
(fun type_err gl ->
tclTHEN
(tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr
- (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr))
+ (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr))
(fun gl -> raise type_err)
gl))
(old_cleartac clr)
@@ -1441,7 +1446,7 @@ let tclINTRO_ANON = tclINTRO ~id:None ~conclusion:return
let tclRENAME_HD_PROD name = Goal.enter begin fun gl ->
let convert_concl_no_check t =
- Tactics.convert_concl_no_check t Term.DEFAULTcast in
+ Tactics.convert_concl_no_check t DEFAULTcast in
let concl = Goal.concl gl in
let sigma = Goal.sigma gl in
match EConstr.kind sigma concl with
@@ -1500,7 +1505,7 @@ let tclOPTION o d =
let tacIS_INJECTION_CASE ?ty t = begin
tclOPTION ty (tacTYPEOF t) >>= fun ty ->
tacREDUCE_TO_QUANTIFIED_IND ty >>= fun ((mind,_),_) ->
- tclUNIT (Globnames.eq_gr (Globnames.IndRef mind) (Coqlib.build_coq_eq ()))
+ tclUNIT (GlobRef.equal (GlobRef.IndRef mind) (Coqlib.build_coq_eq ()))
end
let tclWITHTOP tac = Goal.enter begin fun gl ->
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 2b8f1d5409..9ba23467e7 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -212,7 +212,7 @@ val pf_abs_prod :
EConstr.t -> Goal.goal Evd.sigma * EConstr.types
val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
-val mkSsrRef : string -> Globnames.global_reference
+val mkSsrRef : string -> GlobRef.t
val mkSsrConst :
string ->
env -> evar_map -> evar_map * EConstr.t
@@ -224,7 +224,7 @@ val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
val pf_fresh_global :
- Globnames.global_reference ->
+ GlobRef.t ->
Goal.goal Evd.sigma ->
Constr.constr * Goal.goal Evd.sigma
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 717657a247..83b4d65628 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -14,6 +14,7 @@ open Util
open Names
open Printer
open Term
+open Constr
open Termops
open Globnames
open Misctypes
@@ -356,7 +357,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in
let ty_ev = Evar.Set.fold (fun i e ->
let ex = i in
- let i_ty = EConstr.of_constr (Evd.evar_concl (Evd.find (project gl) ex)) in
+ let i_ty = Evd.evar_concl (Evd.find (project gl) ex) in
Evar.Set.union e (evars_of_term i_ty))
ev Evar.Set.empty in
let inter = Evar.Set.inter ev ty_ev in
@@ -418,7 +419,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with
let is_injection_case c gl =
let gl, cty = pfe_type_of gl c in
let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in
- eq_gr (IndRef mind) (Coqlib.build_coq_eq ())
+ GlobRef.equal (IndRef mind) (Coqlib.build_coq_eq ())
let perform_injection c gl =
let gl, cty = pfe_type_of gl c in
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 57635edac4..f929e94309 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl =
let foldtac occ rdx ft gl =
let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
let sigma, t = ft in
- let t = EConstr.to_constr sigma t in
+ let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
let fold, conclude = match rdx with
| Some (_, (In_T _ | In_X_In_T _)) | None ->
let ise = Evd.create_evar_defs sigma in
@@ -287,7 +287,10 @@ let foldtac occ rdx ft gl =
(fun env c _ h -> try find_T env c h ~k:(fun env t _ _ -> t) with NoMatch ->c),
(fun () -> try end_T () with NoMatch -> fake_pmatcher_end ())
| _ ->
- (fun env c _ h -> try let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in EConstr.to_constr sigma (EConstr.of_constr t)
+ (fun env c _ h ->
+ try
+ let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in
+ EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc ()
++ str "does not match redex " ++ pr_constr_pat c)),
fake_pmatcher_end in
@@ -359,7 +362,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in
let open_evs = List.filter (fun k ->
Sorts.InProp <> Retyping.get_sort_family_of
- env sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))))
+ env sigma (Evd.evar_concl (Evd.find sigma k)))
evs in
if open_evs <> [] then Some name else None)
(List.combine (Array.to_list args) names)
@@ -369,8 +372,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
;;
let is_construct_ref sigma c r =
- EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r
-let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r
+ EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
+let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
let rwcltac cl rdx dir sr gl =
let n, r_n,_, ucst = pf_abs_evars gl sr in
@@ -435,7 +438,7 @@ let lz_setoid_relation =
| env', srel when env' == env -> srel
| _ ->
let srel =
- try Some (Universes.constr_of_global @@
+ try Some (UnivGen.constr_of_global @@
Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation")
with _ -> None in
last_srel := (env, srel); srel
@@ -478,11 +481,11 @@ let rwprocess_rule dir rule gl =
| _ -> let ra = Array.append a [|r|] in
function 1 ->
let sigma, pi1 = Evd.fresh_global env sigma coq_prod.Coqlib.proj1 in
- EConstr.mkApp (EConstr.of_constr pi1, ra), sigma
+ EConstr.mkApp (pi1, ra), sigma
| _ ->
let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
- EConstr.mkApp (EConstr.of_constr pi2, ra), sigma in
- if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then
+ EConstr.mkApp (pi2, ra), sigma in
+ if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then
let s, sigma = sr sigma 2 in
loop (converse_dir d) sigma s a.(1) rs 0
else
@@ -557,7 +560,7 @@ let rwrxtac occ rdx_pat dir rule gl =
let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
let sigma, pat =
let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in
- mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in
+ mk_tpattern env sigma0 (sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma r) (rw_progress rhs) d (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in
sigma, pats @ [pat] in
let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in
@@ -567,7 +570,7 @@ let rwrxtac occ rdx_pat dir rule gl =
let r = ref None in
(fun env c _ h -> do_once r (fun () -> find_rule (EConstr.of_constr c), c); mkRel h),
(fun concl -> closed0_check concl e gl;
- let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ev c)) , x) in
+ let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ~abort_on_undefined_evars:false ev c)) , x) in
let concl0 = EConstr.Unsafe.to_constr concl0 in
let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
let (d, r), rdx = conclude concl in
@@ -589,7 +592,10 @@ let ssrinstancesofrule ist dir arg gl =
let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
let sigma, pat =
let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in
- mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in
+ mk_tpattern env sigma0
+ (sigma,EConstr.to_constr ~abort_on_undefined_evars:false sigma r)
+ (rw_progress rhs) d
+ (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in
sigma, pats @ [pat] in
let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 6e17e8e158..c6beb08c5e 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -184,9 +184,7 @@ let havetac ist
let gs =
List.map (fun (_,a) ->
Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in
- let tacopen_skols gl =
- let stuff, g = Refiner.unpackage gl in
- Refiner.repackage stuff (gs @ [g]) in
+ let tacopen_skols gl = re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma in
let gl, ty = pf_e_type_of gl t in
gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id,
Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac)
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 7897cb1700..8207bc11e0 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -12,6 +12,7 @@ open Ssrmatching_plugin
open Util
open Names
+open Constr
open Proofview
open Proofview.Notations
@@ -90,11 +91,11 @@ open State
(** Warning: unlike [nb_deps_assums], it does not perform reduction *)
let rec nb_assums cur env sigma t =
match EConstr.kind sigma t with
- | Term.Prod(name,ty,body) ->
+ | Prod(name,ty,body) ->
nb_assums (cur+1) env sigma body
- | Term.LetIn(name,ty,t1,t2) ->
+ | LetIn(name,ty,t1,t2) ->
nb_assums (cur+1) env sigma t2
- | Term.Cast(t,_,_) ->
+ | Cast(t,_,_) ->
nb_assums cur env sigma t
| _ -> cur
let nb_assums = nb_assums 0
@@ -218,15 +219,16 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
Ssrview.tclIPAT_VIEWS ~views:l
~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats)
| IPatDispatch ipatss ->
- tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) []
+ tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) []
| IPatId id -> Ssrcommon.tclINTRO_ID id
| IPatCase ipatss ->
- tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss
+ tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss
| IPatInj ipatss ->
tclIORPAT (Ssrcommon.tclWITHTOP
- (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) ipatss
+ (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t)))
+ future_ipats ipatss
| IPatAnon Drop -> intro_drop
| IPatAnon One -> Ssrcommon.tclINTRO_ANON
@@ -254,17 +256,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatTac t -> t
-and ipat_tac pl : unit tactic =
+and ipat_tac future_ipats pl : unit tactic =
match pl with
| [] -> tclUNIT ()
| pat :: pl ->
- Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 pl)) <*>
+ Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*>
isTICK pat <*>
- ipat_tac pl
+ ipat_tac future_ipats pl
-and tclIORPAT tac = function
+and tclIORPAT tac future_ipats = function
| [[]] -> tac
- | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p)
+ | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p)
let split_at_first_case ipats =
let rec loop acc = function
@@ -285,7 +287,7 @@ let main ?eqtac ~first_case_is_dispatch ipats =
let case = ssr_exception first_case_is_dispatch case in
let case = option_to_list case in
let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in
- Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
+ Ssrcommon.tcl0G (ipat_tac [] (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
end (* }}} *)
@@ -418,7 +420,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
Goal.enter_one begin fun g ->
let pat = Ssrmatching.interp_cpattern sigma0 t None in
let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in
- let cl = EConstr.to_constr sigma cl0 in
+ let cl = EConstr.to_constr ~abort_on_undefined_evars:false sigma cl0 in
let (c, ucst), cl =
try Ssrmatching.fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
with Ssrmatching.NoMatch -> Ssrmatching.redex_of_pattern env pat, cl in
@@ -555,7 +557,7 @@ let rec eqmoveipats eqpat = function
let ssrsmovetac = Goal.enter begin fun g ->
let sigma, concl = Goal.(sigma g, concl g) in
match EConstr.kind sigma concl with
- | Term.Prod _ | Term.LetIn _ -> tclUNIT ()
+ | Prod _ | LetIn _ -> tclUNIT ()
| _ -> Tactics.hnf_in_concl
end
@@ -593,8 +595,8 @@ let rec is_Evar_or_CastedMeta sigma x =
let occur_existential_or_casted_meta sigma c =
let rec occrec c = match EConstr.kind sigma c with
- | Term.Evar _ -> raise Not_found
- | Term.Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found
+ | Evar _ -> raise Not_found
+ | Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found
| _ -> EConstr.iter sigma occrec c
in
try occrec c; false
@@ -623,8 +625,8 @@ let tacFIND_ABSTRACT_PROOF check_lock abstract_n =
Goal.enter_one ~__LOC__ begin fun g ->
let sigma, env = Goal.(sigma g, env g) in
let l = Evd.fold_undefined (fun e ei l ->
- match EConstr.kind sigma (EConstr.of_constr ei.Evd.evar_concl) with
- | Term.App(hd, [|ty; n; lock|])
+ match EConstr.kind sigma ei.Evd.evar_concl with
+ | App(hd, [|ty; n; lock|])
when (not check_lock ||
(occur_existential_or_casted_meta sigma ty &&
is_Evar_or_CastedMeta sigma lock)) &&
@@ -653,8 +655,8 @@ let ssrabstract dgens =
let sigma, env, concl = Goal.(sigma g, env g, concl g) in
let t = args_id.(0) in
match EConstr.kind sigma t with
- | (Term.Evar _ | Term.Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id
- | Term.Cast(m,_,_)
+ | (Evar _ | Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id
+ | Cast(m,_,_)
when EConstr.isEvar sigma m || EConstr.isMeta sigma m ->
Ssrcommon.tacUNIFY concl t <*> tclUNIT id
| _ ->
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 5f39674407..fbfbdb1108 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -10,6 +10,7 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+let _vmcast = Constr.VMcast
open Names
open Pp
open Pcoq
@@ -17,7 +18,6 @@ open Ltac_plugin
open Genarg
open Stdarg
open Tacarg
-open Term
open Libnames
open Tactics
open Tacmach
@@ -64,7 +64,7 @@ DECLARE PLUGIN "ssreflect_plugin"
* we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = CLexer.get_keyword_state () ;;
-let tacltop = (5,Notation_term.E)
+let tacltop = (5,Notation_gram.E)
let pr_ssrtacarg _ _ prt = prt tacltop
ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg
@@ -1938,7 +1938,7 @@ END
let vmexacttac pf =
Goal.nf_enter begin fun gl ->
- exact_no_check (EConstr.mkCast (pf, VMcast, Tacmach.New.pf_concl gl))
+ exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl))
end
TACTIC EXTEND ssrexact
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 2ac7c7e264..7cd3751cef 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -14,11 +14,11 @@ open Ltac_plugin
val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
+val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 9cc4f5cece..372ae86bda 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -11,6 +11,7 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
open Names
+open Constr
open Termops
open Tacmach
open Misctypes
@@ -32,9 +33,8 @@ let get_index = function ArgArg i -> i | _ ->
let tclPERM perm tac gls =
let subgls = tac gls in
- let sigma, subgll = Refiner.unpackage subgls in
- let subgll' = perm subgll in
- Refiner.repackage sigma subgll'
+ let subgll' = perm subgls.Evd.it in
+ re_sig subgll' subgls.Evd.sigma
let rot_hyps dir i hyps =
let n = List.length hyps in
@@ -104,10 +104,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
- | Term.Var id when hidden_clseq clseq && id = gl_id -> cl0
- | Term.Prod (Name id, t, c') when List.mem_assoc id id_map ->
+ | Var id when hidden_clseq clseq && id = gl_id -> cl0
+ | Prod (Name id, t, c') when List.mem_assoc id id_map ->
EConstr.mkProd (Name (orig_id id), unmark t, unmark c')
- | Term.LetIn (Name id, v, t, c') when List.mem_assoc id id_map ->
+ | 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 05dbf0a86d..750461a1bf 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -19,7 +19,7 @@ open Constrexpr_ops
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Vernac_
+open Pvernac.Vernac_
open Ltac_plugin
open Notation_ops
open Notation_term
@@ -377,7 +377,10 @@ let interp_head_pat hpat =
| Cast (c', _, _) -> loop c'
| Prod (_, _, c') -> loop c'
| LetIn (_, _, _, c') -> loop c'
- | _ -> Constr_matching.is_matching (Global.env()) Evd.empty p (EConstr.of_constr c) in
+ | _ ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Constr_matching.is_matching env sigma p (EConstr.of_constr c) in
filter_head, loop
let all_true _ = true
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index aa614fbc11..29a936381f 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -254,18 +254,18 @@ let finalize_view s0 ?(simple_types=true) p =
Goal.enter_one ~__LOC__ begin fun g ->
let env = Goal.env g in
let sigma = Goal.sigma g in
- let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in
+ let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
let filter x _ = Evar.Set.mem x evars_of_p in
let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
let p = Reductionops.nf_evar sigma p in
let get_body = function Evd.Evar_defined x -> x | _ -> assert false in
let evars_of_econstr sigma t =
- Evd.evars_of_term (EConstr.to_constr sigma (EConstr.of_constr t)) in
+ Evarutil.undefined_evars_of_term sigma (EConstr.of_constr t) in
let rigid_of s =
List.fold_left (fun l k ->
if Evd.is_defined sigma k then
let bo = get_body Evd.(evar_body (find sigma k)) in
- k :: l @ Evar.Set.elements (evars_of_econstr sigma bo)
+ k :: l @ Evar.Set.elements (evars_of_econstr sigma (EConstr.Unsafe.to_constr bo))
else l
) [] s in
let und0 = (* Unassigned evars in the initial goal *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 21:15:43 +0000