aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrast.mli2
-rw-r--r--plugins/ssr/ssrcommon.ml46
-rw-r--r--plugins/ssr/ssrcommon.mli4
-rw-r--r--plugins/ssr/ssrelim.ml7
-rw-r--r--plugins/ssr/ssrequality.ml30
-rw-r--r--plugins/ssr/ssrfwd.ml5
-rw-r--r--plugins/ssr/ssripats.ml52
-rw-r--r--plugins/ssr/ssrparser.ml453
-rw-r--r--plugins/ssr/ssrparser.mli4
-rw-r--r--plugins/ssr/ssrtacticals.ml15
-rw-r--r--plugins/ssr/ssrtacticals.mli4
-rw-r--r--plugins/ssr/ssrvernac.ml48
-rw-r--r--plugins/ssr/ssrview.ml8
13 files changed, 123 insertions, 115 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 7f5f2f63d..5571c5420 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod
type ssrocc = (bool * int list) option
(* index MAYBE REMOVE ONLY INTERNAL stuff between {} *)
-type ssrindex = int Misctypes.or_var
+type ssrindex = int Locus.or_var
(* clear switch {H G} *)
type ssrclear = ssrhyps
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d5118da4c..2a31157be 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,10 +181,9 @@ let option_assert_get o msg =
(** Constructors for rawconstr *)
open Glob_term
open Globnames
-open Misctypes
open Decl_kinds
-let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None)
+let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else []
let rec isRHoles cl = match cl with
@@ -254,7 +253,7 @@ let interp_refine ist gl rc =
let interp_open_constr ist gl gc =
- let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in
+ let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in
(project gl, (sigma, c))
let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c)
@@ -423,12 +422,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 +503,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 +569,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 +582,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 +747,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 +801,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 =
@@ -856,8 +860,8 @@ let mkCProp loc = CAst.make ?loc @@ CSort GProp
let mkCType loc = CAst.make ?loc @@ CSort (GType [])
let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None)
let rec mkCHoles ?loc n =
- if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
-let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
+ if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
+let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)
let mkCLambda ?loc name ty t = CAst.make ?loc @@
CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
let mkCArrow ?loc ty t = CAst.make ?loc @@
@@ -980,7 +984,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 +1220,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 +1445,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 +1504,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 2b8f1d540..9ba23467e 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 717657a24..fbe3b000f 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -14,9 +14,10 @@ open Util
open Names
open Printer
open Term
+open Constr
open Termops
open Globnames
-open Misctypes
+open Tactypes
open Tacmach
open Ssrmatching_plugin
@@ -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 57635edac..f929e9430 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 6e17e8e15..2c046190f 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -86,7 +86,6 @@ let _ =
open Constrexpr
open Glob_term
-open Misctypes
let combineCG t1 t2 f g = match t1, t2 with
| (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
@@ -184,9 +183,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 42566575c..8207bc11e 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
@@ -133,6 +134,12 @@ let intro_clear ids future_ipats =
isCLR_PUSHL clear_ids
end
+let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl ->
+ let ctx = Goal.hyps gl in
+ List.iter (Ssrcommon.check_hyp_exists ctx) hyps;
+ tclUNIT ()
+end
+
(** [=> []] *****************************************************************)
let tac_case t =
Goal.enter begin fun _ ->
@@ -212,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
@@ -229,7 +237,9 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatNoop -> tclUNIT ()
| IPatSimpl Nop -> tclUNIT ()
- | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
+ | IPatClear ids ->
+ tacCHECK_HYPS_EXIST ids <*>
+ intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
| IPatSimpl (Simpl n) ->
V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
@@ -246,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
@@ -277,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 (* }}} *)
@@ -410,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
@@ -547,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
@@ -585,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
@@ -615,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)) &&
@@ -645,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 0d82a9f09..352f88bb3 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,18 +18,19 @@ open Ltac_plugin
open Genarg
open Stdarg
open Tacarg
-open Term
open Libnames
open Tactics
open Tacmach
open Util
+open Locus
open Tacexpr
open Tacinterp
open Pltac
open Extraargs
open Ppconstr
-open Misctypes
+open Namegen
+open Tactypes
open Decl_kinds
open Constrexpr
open Constrexpr_ops
@@ -64,7 +66,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
@@ -301,24 +303,24 @@ END
let pr_index = function
- | Misctypes.ArgVar {CAst.v=id} -> pr_id id
- | Misctypes.ArgArg n when n > 0 -> int n
+ | ArgVar {CAst.v=id} -> pr_id id
+ | ArgArg n when n > 0 -> int n
| _ -> mt ()
let pr_ssrindex _ _ _ = pr_index
-let noindex = Misctypes.ArgArg 0
+let noindex = ArgArg 0
let check_index ?loc i =
if i > 0 then i else CErrors.user_err ?loc (str"Index not positive")
let mk_index ?loc = function
- | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i)
+ | ArgArg i -> ArgArg (check_index ?loc i)
| iv -> iv
let interp_index ist gl idx =
Tacmach.project gl,
match idx with
- | Misctypes.ArgArg _ -> idx
- | Misctypes.ArgVar id ->
+ | ArgArg _ -> idx
+ | ArgVar id ->
let i =
try
let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
@@ -336,7 +338,7 @@ let interp_index ist gl idx =
| None -> raise Not_found
end end
with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
- Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
+ ArgArg (check_index ?loc:id.CAst.loc i)
open Pltac
@@ -543,7 +545,7 @@ END
let remove_loc x = x.CAst.v
-let ipat_of_intro_pattern p = Misctypes.(
+let ipat_of_intro_pattern p = Tactypes.(
let rec ipat_of_intro_pattern = function
| IntroNaming (IntroIdentifier id) -> IPatId id
| IntroAction IntroWildcard -> IPatAnon Drop
@@ -585,37 +587,25 @@ let pr_ssripat _ _ _ = pr_ipat
let pr_ssripats _ _ _ = pr_ipats
let pr_ssriorpat _ _ _ = pr_iorpat
-(*
-let intern_ipat ist ipat =
- let rec check_pat = function
- | IPatClear clr -> ignore (List.map (intern_hyp ist) clr)
- | IPatCase iorpat -> List.iter (List.iter check_pat) iorpat
- | IPatDispatch iorpat -> List.iter (List.iter check_pat) iorpat
- | IPatInj iorpat -> List.iter (List.iter check_pat) iorpat
- | _ -> () in
- check_pat ipat; ipat
-*)
-
let intern_ipat ist =
map_ipat
(fun id -> id)
- (intern_hyp ist) (* TODO: check with ltac, old code was ignoring the result *)
+ (intern_hyp ist)
(glob_ast_closure_term ist)
let intern_ipats ist = List.map (intern_ipat ist)
let interp_intro_pattern = interp_wit wit_intro_pattern
-let interp_introid ist gl id = Misctypes.(
+let interp_introid ist gl id =
try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id))))))
with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v
-)
let get_intro_id = function
| IntroNaming (IntroIdentifier id) -> id
| _ -> assert false
-let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
+let rec add_intro_pattern_hyps ipat hyps =
let {CAst.loc=loc;v=ipat} = ipat in
match ipat with
| IntroNaming (IntroIdentifier id) ->
@@ -634,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
| IntroForthcoming _ ->
(* As in ipat_of_intro_pattern, was unable to determine which kind
of ipat interp_introid could return [HH] *) assert false
-)
(* We interp the ipat using the standard ltac machinery for ids, since
* we have no clue what a name could be bound to (maybe another ipat) *)
@@ -1075,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
| BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
let bs, c' = format_constr_expr h c in
Bdef (x, oty, v) :: bs, c'
- | [BFcast], { v = CCast (c, CastConv t) } ->
+ | [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
[Bcast t], c
| BFrec (has_str, has_cast) :: h,
{ v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
@@ -1104,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
let mkFwdVal fk c = ((fk, []), c)
let mkssrFwdVal fk c = ((fk, []), (c,None))
-let dC t = CastConv t
+let dC t = Glob_term.CastConv t
let same_ist { interp_env = x } { interp_env = y } =
match x,y with
@@ -1221,8 +1210,8 @@ let push_binders c2 bs =
| [] -> c
| _ -> anomaly "binder not a lambda nor a let in" in
match c2 with
- | { loc; v = CCast (ct, CastConv cty) } ->
- CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs)))
+ | { loc; v = CCast (ct, Glob_term.CastConv cty) } ->
+ CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs)))
| ct -> loop false ct bs
let rec fix_binders = let open CAst in function
@@ -1949,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 2ac7c7e26..7cd3751ce 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 9cc4f5cec..83581f341 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -11,9 +11,9 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
open Names
+open Constr
open Termops
open Tacmach
-open Misctypes
open Locusops
open Ssrast
@@ -24,7 +24,7 @@ module NamedDecl = Context.Named.Declaration
(** Tacticals (+, -, *, done, by, do, =>, first, and last). *)
-let get_index = function ArgArg i -> i | _ ->
+let get_index = function Locus.ArgArg i -> i | _ ->
anomaly "Uninterpreted index"
(* Toplevel constr must be globalized twice ! *)
@@ -32,9 +32,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 +103,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/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index a5636ad0f..684e00235 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -17,7 +17,7 @@ val tclSEQAT :
Tacinterp.interp_sign ->
Tacinterp.Value.t ->
Ssrast.ssrdir ->
- int Misctypes.or_var *
+ int Locus.or_var *
(('a * Tacinterp.Value.t option list) *
Tacinterp.Value.t option) ->
Tacmach.tactic
@@ -37,7 +37,7 @@ val hinttac :
val ssrdotac :
Tacinterp.interp_sign ->
- ((int Misctypes.or_var * Ssrast.ssrmmod) *
+ ((int Locus.or_var * Ssrast.ssrmmod) *
(bool * Tacinterp.Value.t option list)) *
((Ssrast.ssrhyps *
((Ssrast.ssrhyp_or_id * string) *
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 05dbf0a86..939e97866 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
@@ -27,7 +27,6 @@ open Glob_term
open Globnames
open Stdarg
open Genarg
-open Misctypes
open Decl_kinds
open Libnames
open Pp
@@ -377,7 +376,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 aa614fbc1..faebe3179 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p =
let mkGHole =
DAst.make
- (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None))
+ (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None))
let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
let mkGApp f args =
if args = [] then f
@@ -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.39.1) at 2024-08-09 22:15:05 +0000