diff options
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 32 |
1 files changed, 10 insertions, 22 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 11ebe4337..859513d5c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) @@ -141,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 @@ -382,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 @@ -617,20 +605,20 @@ let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = let fail = ref false in - let interp_rpattern ist gl gc = - try interp_rpattern ist gl gc + let interp_rpattern gl gc = + try interp_rpattern gl gc with _ when snd mult = May -> fail := true; project gl, T mkProp in let interp gc gl = try interp_term ist gl gc with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in let rwtac gl = - let rx = Option.map (interp_rpattern ist gl) grx in + let rx = Option.map (interp_rpattern gl) grx in let t = interp gt 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 | RWeq -> rwrxtac occ rx dir t) gl in - let ctac = cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in + let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl (** Rewrite argument sequence *) |