aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrast.mli12
-rw-r--r--plugins/ssr/ssrbwd.mli2
-rw-r--r--plugins/ssr/ssrcommon.ml14
-rw-r--r--plugins/ssr/ssrcommon.mli2
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--plugins/ssr/ssrequality.ml16
-rw-r--r--plugins/ssr/ssrfun.v5
-rw-r--r--plugins/ssr/ssripats.mli6
-rw-r--r--plugins/ssr/ssrparser.ml46
-rw-r--r--plugins/ssr/ssrparser.mli13
-rw-r--r--plugins/ssr/ssrtacticals.ml4
-rw-r--r--plugins/ssr/ssrvernac.ml46
12 files changed, 45 insertions, 43 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 9783bc61d..7f5f2f63d 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -138,7 +138,7 @@ type ssrclseq = InGoal | InHyps
type 'tac ssrhint = bool * 'tac option list
type 'tac fwdbinders =
- bool * (ssrhpats * ((ssrfwdfmt * ssrterm) * 'tac ssrhint))
+ bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
type clause =
(ssrclear * ((ssrhyp_or_id * string) *
@@ -157,13 +157,15 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
open Ssrmatching_plugin
open Ssrmatching
+
+type 'a ssrcasearg = ssripat option * ('a * ssripats)
+type 'a ssrmovearg = ssrview * 'a ssrcasearg
+
type ssrdgens = { dgens : (ssrdocc * cpattern) list;
gens : (ssrdocc * cpattern) list;
clr : ssrclear }
-type ssrcasearg = ssripat option * (ssrdgens * ssripats)
-type ssrmovearg = ssrview * ssrcasearg
-type ssragens = ((ssrhyps option * occ) * ssrterm) list list * ssrclear
-type ssrapplyarg = ssrterm list * (ssragens * ssripats)
+type 'a ssragens = (ssrdocc * 'a) list list * ssrclear
+type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
(* OOP : these are general shortcuts *)
type gist = Tacintern.glob_sign
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index 6243e5e68..694ecfa37 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -13,4 +13,4 @@ open Proofview
val apply_top_tac : unit tactic
-val inner_ssrapplytac : ssrterm list -> ssragens -> ist -> unit tactic
+val inner_ssrapplytac : ssrterm list -> ssrterm ssragens -> ist -> unit tactic
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5163ec7b3..f049963f1 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -460,7 +460,7 @@ let red_product_skip_id env sigma c = match EConstr.kind sigma c with
let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac
-(** Open term to lambda-term coercion {{{ ************************************)
+(** Open term to lambda-term coercion *)(* {{{ ************************************)
(* This operation takes a goal gl and an open term (sigma, t), and *)
(* returns a term t' where all the new evars in sigma are abstracted *)
@@ -768,7 +768,7 @@ let discharge_hyp (id', (id, mode)) gl =
let cl' = Vars.subst_var id (pf_concl gl) in
match pf_get_hyp gl id, mode with
| NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" ->
- Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl')))
+ Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl')))
[EConstr.of_constr (mkVar id)]) gl
| NamedDecl.LocalDef (_, v, t), _ ->
Proofview.V82.of_tactic
@@ -1000,7 +1000,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
with e when CErrors.noncritical e -> raise dependent_apply_error
-(** Profiling {{{ *************************************************************)
+(** Profiling *)(* {{{ *************************************************************)
type profiler = {
profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
reset : unit -> unit;
@@ -1128,7 +1128,7 @@ let interp_clr sigma = function
(** Basic tacticals *)
-(** Multipliers {{{ ***********************************************************)
+(** Multipliers *)(* {{{ ***********************************************************)
(* tactical *)
@@ -1168,7 +1168,7 @@ let tclMULT = function
let old_cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (Tactics.clear (hyps_ids clr))
let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr)
-(** }}} *)
+(* }}} *)
(** Generalize tactic *)
@@ -1193,13 +1193,13 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
else let gl, ccl = pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl
else if to_ind && occ = None then
let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in
- let ucst = Evd.union_evar_universe_context ucst ucst' in
+ let ucst = UState.union ucst ucst' in
if nv = 0 then anomaly "occur_existential but no evars" else
let gl, pty = pfe_type_of gl p in
false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl
else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match")
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
+let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs)
let genclrtac cl cs clr =
let tclmyORELSE tac1 tac2 gl =
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 7c16e1ba9..2b8f1d540 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -414,6 +414,8 @@ val clr_of_wgen :
val unfold : EConstr.t list -> unit Proofview.tactic
+val apply_type : EConstr.types -> EConstr.t list -> Proofview.V82.tac
+
(* New code ****************************************************************)
(* To call old code *)
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 33ebe26b6..717657a24 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -30,8 +30,6 @@ module RelDecl = Context.Rel.Declaration
(** The "case" and "elim" tactic *)
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
-
(* TASSI: given the type of an elimination principle, it finds the higher order
* argument (index), it computes it's arity and the arity of the eliminator and
* checks if the eliminator is recursive or not *)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 71cde0ca1..57635edac 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -143,18 +143,6 @@ let newssrcongrtac arg ist gl =
(** 7. Rewriting tactics (rewrite, unlock) *)
-(** Coq rewrite compatibility flag *)
-
-
-let _ =
- let ssr_strict_match = ref false in
- Goptions.declare_bool_option
- { Goptions.optname = "strict redex matching";
- Goptions.optkey = ["Match"; "Strict"];
- Goptions.optread = (fun () -> !ssr_strict_match);
- Goptions.optdepr = true; (* noop *)
- Goptions.optwrite = (fun b -> ssr_strict_match := b) }
-
(** Rewrite rules *)
type ssrwkind = RWred of ssrsimpl | RWdef | RWeq
@@ -228,7 +216,7 @@ let same_proj sigma t1 t2 =
let all_ok _ _ = true
let fake_pmatcher_end () =
- mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp)
+ mkProp, L2R, (Evd.empty, UState.empty, mkProp)
let unfoldintac occ rdx t (kt,_) gl =
let fs sigma x = Reductionops.nf_evar sigma x in
@@ -384,8 +372,6 @@ 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
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
-
let rwcltac cl rdx dir sr gl =
let n, r_n,_, ucst = pf_abs_evars gl sr in
let r_n' = pf_abs_cterm gl n r_n in
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 96b6ed295..ac2c78249 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -165,7 +165,7 @@ Require Import ssreflect.
(* rev_right_loop inv op <-> op, inv obey the inverse loop reverse right *)
(* axiom: (x op y) op (inv y) = x for all x, y. *)
(* Note that familiar "cancellation" identities like x + y - y = x or *)
-(* x - y + x = x are respectively instances of right_loop and rev_right_loop *)
+(* x - y + y = x are respectively instances of right_loop and rev_right_loop *)
(* The corresponding lemmas will use the K and NK/VK suffixes, respectively. *)
(* *)
(* - Morphisms for functions and relations: *)
@@ -639,6 +639,9 @@ End Injections.
Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed.
+(* Force implicits to use as a view. *)
+Prenex Implicits Some_inj.
+
(* cancellation lemmas for dependent type casts. *)
Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).
Proof. by case: y /. Qed.
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index b8716c0c4..89cba4be7 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -29,11 +29,11 @@ val tclIPATssr : ssripats -> unit Proofview.tactic
[tac E: gens => ipats]
where [E] is injected into [ipats] (at the right place) and [gens] are
generalized before calling [tac] *)
-val ssrmovetac : ssrmovearg -> unit Proofview.tactic
+val ssrmovetac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrsmovetac : unit Proofview.tactic
-val ssrelimtac : ssrmovearg -> unit Proofview.tactic
+val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrselimtoptac : unit Proofview.tactic
-val ssrcasetac : ssrmovearg -> unit Proofview.tactic
+val ssrcasetac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrscasetoptac : unit Proofview.tactic
(* The implementation of abstract: is half here, for the [[: var ]]
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 70f73c1fe..2bed8b624 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -952,7 +952,7 @@ let pr_ssrhint _ _ = pr_hint
ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint
| [ ] -> [ nohint ]
END
-(** The "in" pseudo-tactical {{{ **********************************************)
+(** The "in" pseudo-tactical *)(* {{{ **********************************************)
(* We can't make "in" into a general tactical because this would create a *)
(* crippling conflict with the ltac let .. in construct. Hence, we add *)
@@ -1438,7 +1438,7 @@ let tactic_expr = Pltac.tactic_expr
let old_tac = V82.tactic
-(** Name generation {{{ *******************************************************)
+(** Name generation *)(* {{{ *******************************************************)
(* Since Coq now does repeated internal checks of its external lexical *)
(* rules, we now need to carve ssreflect reserved identifiers out of *)
@@ -1490,7 +1490,7 @@ let _ = add_internal_name (is_tagged perm_tag)
(* We must not anonymize context names discharged by the "in" tactical. *)
-(** Tactical extensions. {{{ **************************************************)
+(** Tactical extensions. *)(* {{{ **************************************************)
(* The TACTIC EXTEND facility can't be used for defining new user *)
(* tacticals, because: *)
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index a52248614..130550388 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -20,3 +20,16 @@ val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c ->
val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
+(* Parsing witnesses, needed to serialize ssreflect syntax *)
+open Ssrmatching_plugin
+open Ssrmatching
+open Ssrast
+open Ssrequality
+
+val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type
+val wit_ssrclauses : clauses Genarg.uniform_genarg_type
+val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type
+val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type
+val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type
+val wit_ssrhavefwdwbinders :
+ (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 21ad6e6ce..9cc4f5cec 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -59,7 +59,7 @@ let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
| L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3
| R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad))
-(** The "in" pseudo-tactical {{{ **********************************************)
+(** The "in" pseudo-tactical *)(* {{{ **********************************************)
let hidden_goal_tag = "the_hidden_goal"
@@ -127,8 +127,6 @@ let endclausestac id_map clseq gl_id cl0 gl =
if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else
errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical")
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
-
let tclCLAUSES tac (gens, clseq) gl =
if clseq = InGoal || clseq = InSeqGoal then tac gl else
let clr_gens = pf_clauseids gl gens clseq in
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index f37452613..e3941c1c5 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -49,7 +49,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;;
(* global syntactic changes and vernacular commands *)
-(** Alternative notations for "match" and anonymous arguments. {{{ ************)
+(** Alternative notations for "match" and anonymous arguments. *)(* {{{ ************)
(* Syntax: *)
(* if <term> is <pattern> then ... else ... *)
@@ -127,7 +127,7 @@ GEXTEND Gram
END
(* }}} *)
-(** Vernacular commands: Prenex Implicits and Search {{{ **********************)
+(** Vernacular commands: Prenex Implicits and Search *)(* {{{ **********************)
(* This should really be implemented as an extension to the implicit *)
(* arguments feature, but unfortuately that API is sealed. The current *)
@@ -461,7 +461,7 @@ END
(* }}} *)
-(** View hint database and View application. {{{ ******************************)
+(** View hint database and View application. *)(* {{{ ******************************)
(* There are three databases of lemmas used to mediate the application *)
(* of reflection lemmas: one for forward chaining, one for backward *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 00:31:56 +0000