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.ml8
-rw-r--r--plugins/ssr/ssrequality.ml12
-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.ml2
-rw-r--r--plugins/ssr/ssrvernac.ml46
10 files changed, 39 insertions, 33 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 511c83269..43c29a08a 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 *)
@@ -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 *)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index f45a191b7..859513d5c 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
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 b29c83eff..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"
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-05-27 10:09:57 +0000