aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml12
-rw-r--r--plugins/ssr/ssrcommon.mli2
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--plugins/ssr/ssrequality.ml2
-rw-r--r--plugins/ssr/ssrfun.v5
-rw-r--r--plugins/ssr/ssrparser.ml46
-rw-r--r--plugins/ssr/ssrtacticals.ml4
-rw-r--r--plugins/ssr/ssrvernac.ml46
8 files changed, 19 insertions, 20 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e2ec8d72a..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 *)
@@ -1199,7 +1199,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
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 7f0b77c9e..57635edac 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -372,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/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/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-05-26 22:27:25 +0000