diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrast.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrbool.v | 20 | ||||
| -rw-r--r-- | plugins/ssr/ssrbwd.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrbwd.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 13 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssreflect.v | 18 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 17 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 14 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrfun.v | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 30 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 13 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.mli | 2 |
26 files changed, 75 insertions, 88 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 0897d3b45b..9e7442caf6 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 49d729bd6c..bf0761d3ae 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -49,7 +49,7 @@ Require Import ssreflect ssrfun. altP (idP my_formula) but circumventing the dependent index capture issue; destructing boolP my_formula generates two subgoals with - assumtions my_formula and ~~ myformula. As + assumptions my_formula and ~~ myformula. As with altP, my_formula must be an application. \unless C, P <-> we can assume property P when a something that holds under condition C (such as C itself). @@ -64,7 +64,7 @@ Require Import ssreflect ssrfun. := forall b : bool, (P -> b) -> b. This is equivalent to ~ (~ P) when P : Prop. implies P Q == wrapper variant type that coerces to P -> Q and - can be used as a P -> Q view unambigously. + can be used as a P -> Q view unambiguously. Useful to avoid spurious insertion of <-> views when Q is a conjunction of foralls, as in Lemma all_and2 below; conversely, avoids confusion in @@ -1003,7 +1003,7 @@ Proof. by case: a; case: b. Qed. Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b. Proof. by case: a; case: b. Qed. -(** Pseudo-cancellation -- i.e, absorbtion **) +(** Pseudo-cancellation -- i.e, absorption **) Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed. Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed. @@ -1245,7 +1245,7 @@ Notation "[ 'pred' x : T | E1 & E2 ]" := (** Coercions for simpl_pred. As simpl_pred T values are used both applicatively and collectively we need simpl_pred to coerce to both pred T _and_ {pred T}. However it is - undesireable to have two distinct constants for what are essentially identical + undesirable to have two distinct constants for what are essentially identical coercion functions, as this confuses the SSReflect keyed matching algorithm. While the Coq Coercion declarations appear to disallow such Coercion aliasing, it is possible to work around this limitation with a combination of modules @@ -1331,9 +1331,9 @@ Variant mem_pred T := Mem of pred T. Similarly to pred_of_simpl, it will usually not be inserted by type inference, as all mem_pred mp =~= pred_sort ?pT unification problems will be solve by the memPredType instance below; pred_of_mem will however - be used if a mem_pred T is used as a {pred T}, which is desireable as it + be used if a mem_pred T is used as a {pred T}, which is desirable as it will avoid a redundant mem in a collective, e.g., passing (mem A) to a lemma - expection a generic collective predicate p : {pred T} and premise x \in P + exception a generic collective predicate p : {pred T} and premise x \in P will display a subgoal x \in A rathere than x \in mem A. Conversely, pred_of_mem will _not_ if it is used id (mem A) is used applicatively or as a pred T; there the simpl_of_mem coercion defined below @@ -1396,7 +1396,7 @@ Notation "[ 'rel' x y 'in' A & B ]" := Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : fun_scope. Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : fun_scope. -(** Aliases of pred T that let us tag intances of simpl_pred as applicative +(** Aliases of pred T that let us tag instances of simpl_pred as applicative or collective, via bespoke coercions. This tagging will give control over the simplification behaviour of inE and othe rewriting lemmas below. For this control to work it is crucial that collective_of_simpl _not_ @@ -1428,7 +1428,7 @@ Implicit Types (mp : mem_pred T). - registered_applicative_pred: this user-facing structure is used to declare values of type pred T meant to be used applicatively. The structure parameter merely displays this same value, and is used to avoid - undesireable, visible occurrence of the structure in the right hand side + undesirable, visible occurrence of the structure in the right hand side of rewrite rules such as app_predE. There is a canonical instance of registered_applicative_pred for values of the applicative_of_simpl coercion, which handles the @@ -1454,7 +1454,7 @@ Implicit Types (mp : mem_pred T). has been fixed earlier by the manifest_mem_pred match. In particular the definition of a predicate using the applicative_pred_of_simpl idiom above will not be expanded - this very case is the reason in_applicative uses - a mem_pred telescope in its left hand side. The more straighforward + a mem_pred telescope in its left hand side. The more straightforward ?x \in applicative_pred_value ?ap (equivalent to in_mem ?x (Mem ?ap)) with ?ap : registered_applicative_pred ?p would set ?p := [pred x | ...] rather than ?p := Apred in the example above. diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 3e0fbc9a8c..f0ae90beca 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index 694ecfa379..e4c7192489 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 56f17703ff..4c95a92022 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -194,8 +194,8 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) let mkRVar id = DAst.make @@ GRef (VarRef id,None) let mkRltacVar id = DAst.make @@ GVar (id) let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv rt) -let mkRType = DAst.make @@ GSort (GType []) -let mkRProp = DAst.make @@ GSort (GProp) +let mkRType = DAst.make @@ GSort (UAnonymous {rigid=true}) +let mkRProp = DAst.make @@ GSort (UNamed [GProp,0]) let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None) let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) @@ -871,8 +871,8 @@ open Constrexpr open Util (** Constructors for constr_expr *) -let mkCProp loc = CAst.make ?loc @@ CSort GProp -let mkCType loc = CAst.make ?loc @@ CSort (GType []) +let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0]) +let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true}) let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) @@ -1119,6 +1119,7 @@ let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) (* XXX the k of the redex should percolate out *) let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = let pat = interp_cpattern gl t None in (* UGLY API *) + let gl = pf_merge_uc_of (fst pat) gl in let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 @@ -1253,6 +1254,7 @@ let abs_wgen keep_let f gen (gl,args,c) = | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in + let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in @@ -1265,6 +1267,7 @@ let abs_wgen keep_let f gen (gl,args,c) = | _, Some ((x, _), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in + let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 575f016014..e920bc318a 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 5e3e8ce5fb..71abafc22f 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -132,7 +132,7 @@ Delimit Scope ssripat_scope with ssripat. Make the general "if" into a notation, so that we can override it below. The notations are "only parsing" because the Coq decompiler will not recognize the expansion of the boolean if; using the default printer - avoids a spurrious trailing %%GEN_IF. **) + avoids a spurious trailing %%GEN_IF. **) Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. @@ -347,10 +347,10 @@ Register protect_term as plugins.ssreflect.protect_term. (** The ssreflect idiom for a non-keyed pattern: - - unkeyed t wiil match any subterm that unifies with t, regardless of + - unkeyed t will match any subterm that unifies with t, regardless of whether it displays the same head symbol as t. - unkeyed t a b will match any application of a term f unifying with t, - to two arguments unifying with with a and b, repectively, regardless of + to two arguments unifying with with a and b, respectively, regardless of apparent head symbols. - unkeyed x where x is a variable will match any subterm with the same type as x (when x would raise the 'indeterminate pattern' error). **) @@ -380,7 +380,7 @@ Notation "=^~ r" := (ssr_converse r) : form_scope. locked_with k t is equal but not convertible to t, much like locked t, but supports explicit tagging with a value k : unit. This is used to mitigate a flaw in the term comparison heuristic of the Coq kernel, - which treats all terms of the form locked t as equal and conpares their + which treats all terms of the form locked t as equal and compares their arguments recursively, leading to an exponential blowup of comparison. For this reason locked_with should be used rather than locked when defining ADT operations. The unlock tactic does not support locked_with @@ -523,7 +523,7 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. elim/abstract_context: (pattern) => G defG. vm_compute; rewrite {}defG {G}. Note that vm_cast are not stored in the proof term - for reductions occuring in the context, hence + for reductions occurring in the context, hence set here := pattern; vm_compute in (value of here) blows up at Qed time. **) Lemma abstract_context T (P : T -> Type) x : @@ -637,7 +637,7 @@ Ltac over := later complain that it cannot erase _top_assumption_ after having abstracted the viewed assumption. Making x and y maximal implicits would avoid this and force the intended @Some_inj nat x y _top_assumption_ - interpretation, but is undesireable as it makes it harder to use Some_inj + interpretation, but is undesirable as it makes it harder to use Some_inj with the many SSReflect and MathComp lemmas that have an injectivity premise. Specifying {T : nonPropType} solves this more elegantly, as then (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop. @@ -655,13 +655,13 @@ Module NonPropType. maybeProp T to tt and use the test_negative instance and set ?r to false. - call_of c r sets up a call to test_of on condition c with expected result r. It has a default instance for its 'callee' projection to Type, which - sets c := maybeProj T and r := false whe unifying with a type T. + sets c := maybeProj T and r := false when unifying with a type T. - type is a telescope on call_of c r, which checks that unifying test_of ?r1 with c indeed sets ?r1 := r; the type structure bundles the 'test' instance and its 'result' value along with its call_of c r projection. The default instance essentially provides eta-expansion for 'type'. This is only essential for the first 'result' projection to bool; using the instance - for other projection merely avoids spurrious delta expansions that would + for other projection merely avoids spurious delta expansions that would spoil the notProp T notation. In detail, unifying T =~= ?S with ?S : nonPropType, i.e., (1) T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 675e4d2457..d0426c86b9 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -96,7 +96,7 @@ let subgoals_tys sigma (relctx, concl) = * (occ, c), deps and the pattern inferred from the type of the eliminator * 3. build the new predicate matching the patterns, and the tactic to * generalize the equality in case eqid is not None - * 4. build the tactic handle intructions and clears as required in ipats and + * 4. build the tactic handle instructions and clears as required in ipats and * by eqid *) let get_eq_type gl = @@ -383,15 +383,22 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in let gl, t = pfe_type_of gl c in let gl, eq = get_eq_type gl in - let gen_eq_tac, gl = + let gen_eq_tac, eq_ty, gl = let refl = EConstr.mkApp (eq, [|t; c; c|]) in let new_concl = EConstr.mkArrow refl Sorts.Relevant (EConstr.Vars.lift 1 (pf_concl orig_gl)) in let new_concl = fire_subst gl new_concl in let erefl, gl = mkRefl t c gl in let erefl = fire_subst gl erefl in - apply_type new_concl [erefl], gl in + let erefl_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl in + let eq_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl_ty in + let gen_eq_tac s = + let open Evd in + let sigma = merge_universe_context s.sigma (evar_universe_context (project gl)) in + apply_type new_concl [erefl] { s with sigma } + in + gen_eq_tac, eq_ty, gl in let rel = k + if c_is_head_p then 1 else 0 in - let src, gl = mkProt EConstr.mkProp EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in + let src, gl = mkProt eq_ty EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in let clr = if deps <> [] then clr else [] in concl, gen_eq_tac, clr, gl diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index a1e2f63b8f..a18df2ced3 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 93c0d5c236..aa1316f15e 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -128,7 +128,7 @@ let newssrcongrtac arg ist gl = x, re_sig si sigma in let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = EConstr.mkApp (arr, lr) in - (* here thw two cases: simple equality or arrow *) + (* here the two cases: simple equality or arrow *) let equality, _, eq_args, gl' = let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in pf_saturate gl (EConstr.of_constr eq) 3 in @@ -313,7 +313,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i (* Coq has a more general form of "equation" (any type with a single *) (* constructor with no arguments with_rect_r elimination lemmas). *) (* However there is no clear way of determining the LHS and RHS of *) -(* such a generic Leibnitz equation -- short of inspecting the type *) +(* such a generic Leibniz equation -- short of inspecting the type *) (* of the elimination lemmas. *) let rec strip_prod_assum c = match Constr.kind c with @@ -336,14 +336,14 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ let sigma, p = (* The resulting goal *) Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in - let elim, gl = + let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = destConst elim in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in - let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in + let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in mkConst c1', gl in let elim = EConstr.of_constr elim in @@ -619,7 +619,11 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt) with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in let rwtac gl = let rx = Option.map (interp_rpattern gl) grx in + let gl = match rx with + | None -> gl + | Some (s,_) -> pf_merge_uc_of s gl in let t = interp gt gl in + let gl = pf_merge_uc_of (fst t) gl in (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 601968d511..43aeeb2dae 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 46af775296..5e600362b4 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 4d4400a0f8..cca94c8c9b 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 6dd01ca6fc..6f8eb51caf 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 3481b25c8b..580c0423e9 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index 893061b154..1d76a9000e 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 27a558611e..858a75698a 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -79,7 +79,6 @@ let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop } ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } END GRAMMAR EXTEND Gram GLOBAL: ssrtacarg; @@ -88,7 +87,6 @@ END (* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *) ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } END GRAMMAR EXTEND Gram GLOBAL: ssrtac3arg; @@ -204,17 +202,6 @@ ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY { pr_ssrhoi } | [ ident(id) ] -> { Id (SsrHyp(Loc.tag ~loc id)) } END -{ - -let pr_ssrhyps _ _ _ = pr_hyps - -} - -ARGUMENT EXTEND ssrhyps TYPED AS ssrhyp list PRINTED BY { pr_ssrhyps } - INTERPRETED BY { interp_hyps } - | [ ssrhyp_list(hyps) ] -> { check_hyps_uniq [] hyps; hyps } -END - (** Rewriting direction *) { @@ -310,18 +297,13 @@ GRAMMAR EXTEND Gram END -ARGUMENT EXTEND ssrsimpl TYPED AS ssrsimplrep PRINTED BY { pr_ssrsimpl } -| [ ssrsimpl_ne(sim) ] -> { sim } -| [ ] -> { Nop } -END - { let pr_ssrclear _ _ _ = pr_clear mt } -ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyps PRINTED BY { pr_ssrclear } +ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyp list PRINTED BY { pr_ssrclear } | [ "{" ne_ssrhyp_list(clr) "}" ] -> { check_hyps_uniq [] clr; clr } END @@ -1005,7 +987,6 @@ let pr_ssrfwdidx _ _ _ = pr_ssrfwdid (* We use a primitive parser for the head identifier of forward *) (* tactis to avoid syntactic conflicts with basic Coq tactics. *) ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY { pr_ssrfwdidx } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -1564,7 +1545,6 @@ let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) = ARGUMENT EXTEND ssrdoarg TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses) PRINTED BY { pr_ssrdoarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -1587,7 +1567,7 @@ let pr_ssrseqarg env sigma _ _ prt = function (* an unindexed tactic. *) ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option)) PRINTED BY { pr_ssrseqarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } + END { @@ -1867,7 +1847,6 @@ let pr_ssrseqdir _ _ _ = function } ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY { pr_ssrseqdir } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END TACTIC EXTEND ssrtclseq @@ -2004,7 +1983,6 @@ let pr_ssreqid _ _ _ = pr_eqid (* We must use primitive parsing here to avoid conflicts with the *) (* basic move, case, and elim tactics. *) ARGUMENT EXTEND ssreqid TYPED AS ssripatrep option PRINTED BY { pr_ssreqid } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -2326,7 +2304,6 @@ let noruleterm loc = mk_term xNoFlag (mkCProp loc) } ARGUMENT EXTEND ssrrule_ne TYPED AS (ssrrwkind * ssrterm) PRINTED BY { pr_ssrrule } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END GRAMMAR EXTEND Gram @@ -2413,7 +2390,6 @@ let pr_ssrrwargs _ _ _ rwargs = pr_list spc pr_rwarg rwargs } ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list PRINTED BY { pr_ssrrwargs } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 4a872be6a5..e6b1706b41 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 5d8c94e49b..f0aed1a934 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 5f20ac2705..e4df7399e1 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 91ff432364..cd2448d764 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index 684e002352..1a9f13cbae 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 08f028465b..279e7ce1a6 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -566,12 +566,10 @@ let print_view_hints env sigma kind l = } VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY -| ![proof] [ "Print" "Hint" "View" ssrviewpos(i) ] -> +| [ "Print" "Hint" "View" ssrviewpos(i) ] -> { - fun ~pstate -> - (* XXX this is incorrect *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in + let env = Global.env () in + let sigma = Evd.from_env env in (match i with | Some k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k) @@ -579,8 +577,7 @@ VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k)) [ Ssrview.AdaptorDb.Forward; Ssrview.AdaptorDb.Backward; - Ssrview.AdaptorDb.Equivalence ]); - pstate + Ssrview.AdaptorDb.Equivalence ]) } END diff --git a/plugins/ssr/ssrvernac.mli b/plugins/ssr/ssrvernac.mli index aa6e02d3eb..994fadcc27 100644 --- a/plugins/ssr/ssrvernac.mli +++ b/plugins/ssr/ssrvernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 0a5c85f4ab..34f13b1096 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index fb9203263a..130bd81d6d 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |