diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-05 20:08:33 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-05 20:09:58 +0100 |
commit | 70e0d022333e0fc9e06b582f6831cbc698959cf0 (patch) | |
tree | 91987abbeb9eb9ac1c26674740412550b80b19bd | |
parent | ebaa67508ec9f59f95e5b68bfece6228e2024ce5 (diff) | |
parent | 18a5eb4ecfcb7c2fbb315719c09e3d5fc0a3574e (diff) |
Generalizing the uses of tactic scopes everywhere.
This feature allows the user to write "let x := open_constr(foo) in ..." for instance
without having to resort to tactic notations. Some changes have been introduced in
the parsing of ad-hoc argument scopes, e.g. one has to put parentheses around
constr:(...) and ltac:(...) in tactics. This breaks badly written scripts, although
it is easy to be forward-compatible by preemptively putting thoses parentheses.
37 files changed, 221 insertions, 220 deletions
@@ -13,6 +13,11 @@ Tactics - In introduction patterns of the form (pat1,...,patn), n should match the exact number of hypotheses introduced (except for local definitions for which pattern can be omitted, as in regular pattern-matching). +- Tactic scopes in Ltac like constr: and ltac: now require parentheses around + their argument. +- Every generic argument type declares a tactic scope of the form "name:(...)" + where name is the name of the argument. This generalizes the constr: and ltac: + instances. Program diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 13f761113..65dc237bb 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -231,8 +231,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< do { Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule - $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$ } - >> ] + $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; + Egramcoq.create_ltac_quotation $se$ + (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v)) + ($lid:s$, None) + } >> ] let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 7366bc03e..f2a567c00 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -180,7 +180,6 @@ type 'a gen_atomic_tactic_expr = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -195,7 +194,6 @@ constraint 'a = < and 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval - | UConstr of 'utrm | Reference of 'ref | TacCall of Loc.t * 'ref * 'a gen_tactic_arg list @@ -206,7 +204,6 @@ and 'a gen_tactic_arg = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -285,7 +282,6 @@ and 'a gen_tactic_expr = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -300,7 +296,6 @@ and 'a gen_tactic_fun_ast = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -313,7 +308,6 @@ constraint 'a = < (** Globalized tactics *) type g_trm = glob_constr_and_expr -type g_utrm = g_trm type g_pat = glob_constr_pattern_and_expr type g_cst = evaluable_global_reference and_short_name or_var type g_ref = ltac_constant located or_var @@ -321,7 +315,6 @@ type g_nam = Id.t located type g_dispatch = < term:g_trm; - utrm:g_utrm; dterm:g_trm; pattern:g_pat; constant:g_cst; @@ -343,7 +336,6 @@ type glob_tactic_arg = (** Raw tactics *) type r_trm = constr_expr -type r_utrm = r_trm type r_pat = constr_pattern_expr type r_cst = reference or_by_notation type r_ref = reference @@ -352,7 +344,6 @@ type r_lev = rlevel type r_dispatch = < term:r_trm; - utrm:r_utrm; dterm:r_trm; pattern:r_pat; constant:r_cst; @@ -374,7 +365,6 @@ type raw_tactic_arg = (** Interpreted tactics *) type t_trm = Term.constr -type t_utrm = Glob_term.closed_glob_constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located @@ -382,7 +372,6 @@ type t_nam = Id.t type t_dispatch = < term:t_trm; - utrm:t_utrm; dterm:g_trm; pattern:t_pat; constant:t_cst; diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 465073b7a..2cf590b1d 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -379,24 +379,27 @@ let with_grammar_rule_protection f x = let ltac_quotations = ref String.Set.empty -let create_ltac_quotation name cast wit e = +let create_ltac_quotation name cast (e, l) = let () = if String.Set.mem name !ltac_quotations then failwith ("Ltac quotation " ^ name ^ " already registered") in let () = ltac_quotations := String.Set.add name !ltac_quotations in + let entry = match l with + | None -> Aentry (name_of_entry e) + | Some l -> Aentryl (name_of_entry e, l) + in (* let level = Some "1" in *) let level = None in - let assoc = Some Extend.RightA in + let assoc = None in let rule = - Next (Next (Next (Stop, + Next (Next (Next (Next (Next (Stop, Atoken (Lexer.terminal name)), Atoken (Lexer.terminal ":")), - Aentry (name_of_entry e)) - in - let action v _ _ loc = - let arg = TacGeneric (Genarg.in_gen (Genarg.rawwit wit) (cast (loc, v))) in - TacArg (loc, arg) + Atoken (Lexer.terminal "(")), + entry), + Atoken (Lexer.terminal ")")) in + let action _ v _ _ _ loc = cast (loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Tactic.tactic_expr None (None, [gram]) + Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram]) diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 17524971f..23eaa64ee 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -62,8 +62,8 @@ val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** {5 Adding tactic quotations} *) -val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) -> - ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit -(** [create_ltac_quotation name f wit e] adds a quotation rule to Ltac, that is, - Ltac grammar now accepts arguments of the form ["name" ":" <e>], and - generates a generic argument using [f] on the entry parsed by [e]. *) +val create_ltac_quotation : string -> + ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Gram.entry * int option) -> unit +(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is, + Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and + generates an argument using [f] on the entry parsed by [e]. *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0fe0ac42b..6eeae925a 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -215,7 +215,7 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | "ltac:"; "("; tac = Tactic.tactic_expr; ")" -> + | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in CHole (!@loc, None, IntroAnonymous, Some arg) ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 0a11d3928..e4ca936a6 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -28,6 +28,7 @@ let arg_of_expr = function let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat +let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c let reference_to_id = function | Libnames.Ident (loc, id) -> (loc, id) @@ -111,10 +112,8 @@ GEXTEND Gram | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (g,n,l) | st = simple_tactic -> st - | IDENT "constr"; ":"; c = Constr.constr -> - TacArg(!@loc,ConstrMayEval(ConstrTerm c)) - | a = tactic_top_or_arg -> TacArg(!@loc,a) - | r = reference; la = LIST0 tactic_arg -> + | a = tactic_arg -> TacArg(!@loc,a) + | r = reference; la = LIST0 tactic_arg_compat -> TacArg(!@loc,TacCall (!@loc,r,la)) ] | "0" [ "("; a = tactic_expr; ")" -> a @@ -138,22 +137,17 @@ GEXTEND Gram body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body) | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] ; - (* Tactic arguments *) - tactic_arg: - [ [ "ltac:"; a = tactic_expr LEVEL "0" -> arg_of_expr a - | "ltac:"; n = natural -> TacGeneric (genarg_of_int n) - | a = tactic_top_or_arg -> a + (* Tactic arguments to the right of an application *) + tactic_arg_compat: + [ [ a = tactic_arg -> a | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) (* Unambigous entries: tolerated w/o "ltac:" modifier *) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; (* Can be used as argument and at toplevel in tactic expressions. *) - tactic_top_or_arg: - [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c - | IDENT "ipattern"; ":"; ipat = simple_intropattern -> - TacGeneric (genarg_of_ipattern ipat) - | c = constr_eval -> ConstrMayEval c + tactic_arg: + [ [ c = constr_eval -> ConstrMayEval c | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l | IDENT "type_term"; c=uconstr -> TacPretype c | IDENT "numgoals" -> TacNumgoals ] ] diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 50e0033e5..ba1f8956e 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -69,7 +69,7 @@ Ltac xpsatz dom d := end in tac. Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. -Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). Ltac psatzl dom := let tac := lazymatch dom with diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index b84cf2540..36511386a 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1492,7 +1492,7 @@ with Simplify := match goal with end. Ltac prove_stable x th := - match constr:x with + match constr:(x) with | ?X1 => unfold term_stable, X1; intros; Simplify; simpl; apply th diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 04decbce1..5f5b97925 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -32,13 +32,13 @@ Qed. Ltac natcst t := match isnatcst t with true => constr:(N.of_nat t) - | _ => constr:InitialRing.NotConstant + | _ => constr:(InitialRing.NotConstant) end. Ltac Ss_to_add f acc := match f with | S ?f1 => Ss_to_add f1 (S acc) - | _ => constr:(acc + f)%nat + | _ => constr:((acc + f)%nat) end. Ltac natprering := diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 8362c8c26..8fcc07716 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -612,32 +612,32 @@ End GEN_DIV. Ltac inv_gen_phi_pos rI add mul t := let rec inv_cst t := match t with - rI => constr:1%positive - | (add rI rI) => constr:2%positive - | (add rI (add rI rI)) => constr:3%positive + rI => constr:(1%positive) + | (add rI rI) => constr:(2%positive) + | (add rI (add rI rI)) => constr:(3%positive) | (mul (add rI rI) ?p) => (* 2p *) match inv_cst p with - NotConstant => constr:NotConstant - | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *) + NotConstant => constr:(NotConstant) + | 1%positive => constr:(NotConstant) (* 2*1 is not convertible to 2 *) | ?p => constr:(xO p) end | (add rI (mul (add rI rI) ?p)) => (* 1+2p *) match inv_cst p with - NotConstant => constr:NotConstant - | 1%positive => constr:NotConstant + NotConstant => constr:(NotConstant) + | 1%positive => constr:(NotConstant) | ?p => constr:(xI p) end - | _ => constr:NotConstant + | _ => constr:(NotConstant) end in inv_cst t. (* The (partial) inverse of gen_phiNword *) Ltac inv_gen_phiNword rO rI add mul opp t := match t with - rO => constr:NwO + rO => constr:(NwO) | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => constr:NotConstant + NotConstant => constr:(NotConstant) | ?p => constr:(Npos p::nil) end end. @@ -646,10 +646,10 @@ End GEN_DIV. (* The inverse of gen_phiN *) Ltac inv_gen_phiN rO rI add mul t := match t with - rO => constr:0%N + rO => constr:(0%N) | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => constr:NotConstant + NotConstant => constr:(NotConstant) | ?p => constr:(Npos p) end end. @@ -657,15 +657,15 @@ End GEN_DIV. (* The inverse of gen_phiZ *) Ltac inv_gen_phiZ rO rI add mul opp t := match t with - rO => constr:0%Z + rO => constr:(0%Z) | (opp ?p) => match inv_gen_phi_pos rI add mul p with - NotConstant => constr:NotConstant + NotConstant => constr:(NotConstant) | ?p => constr:(Zneg p) end | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => constr:NotConstant + NotConstant => constr:(NotConstant) | ?p => constr:(Zpos p) end end. @@ -681,7 +681,7 @@ Ltac inv_gen_phi rO rI cO cI t := end. (* A simple tactic recognizing no constant *) - Ltac inv_morph_nothing t := constr:NotConstant. + Ltac inv_morph_nothing t := constr:(NotConstant). Ltac coerce_to_almost_ring set ext rspec := match type of rspec with @@ -825,31 +825,31 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk := (* Tactic for constant *) Ltac isnatcst t := match t with - O => constr:true + O => constr:(true) | S ?p => isnatcst p - | _ => constr:false + | _ => constr:(false) end. Ltac isPcst t := match t with | xI ?p => isPcst p | xO ?p => isPcst p - | xH => constr:true + | xH => constr:(true) (* nat -> positive *) | Pos.of_succ_nat ?n => isnatcst n - | _ => constr:false + | _ => constr:(false) end. Ltac isNcst t := match t with - N0 => constr:true + N0 => constr:(true) | Npos ?p => isPcst p - | _ => constr:false + | _ => constr:(false) end. Ltac isZcst t := match t with - Z0 => constr:true + Z0 => constr:(true) | Zpos ?p => isPcst p | Zneg ?p => isPcst p (* injection nat -> Z *) @@ -857,7 +857,7 @@ Ltac isZcst t := (* injection N -> Z *) | Z.of_N ?n => isNcst n (* *) - | _ => constr:false + | _ => constr:(false) end. diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v index 6c1a79e4e..54e2789ba 100644 --- a/plugins/setoid_ring/NArithRing.v +++ b/plugins/setoid_ring/NArithRing.v @@ -15,7 +15,7 @@ Set Implicit Arguments. Ltac Ncst t := match isNcst t with true => t - | _ => constr:NotConstant + | _ => constr:(NotConstant) end. Add Ring Nr : Nth (decidable Neqb_ok, constants [Ncst]). diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index a0844100c..77576cb93 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -36,9 +36,9 @@ Qed. Ltac bool_cst t := let t := eval hnf in t in match t with - true => constr:true - | false => constr:false - | _ => constr:NotConstant + true => constr:(true) + | false => constr:(false) + | _ => constr:(NotConstant) end. Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]). diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 914843727..23784cf33 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -17,14 +17,14 @@ Set Implicit Arguments. Ltac Zcst t := match isZcst t with true => t - | _ => constr:NotConstant + | _ => constr:(NotConstant) end. Ltac isZpow_coef t := match t with | Zpos ?p => isPcst p - | Z0 => constr:true - | _ => constr:false + | Z0 => constr:(true) + | _ => constr:(false) end. Notation N_of_Z := Z.to_N (only parsing). @@ -32,7 +32,7 @@ Notation N_of_Z := Z.to_N (only parsing). Ltac Zpow_tac t := match isZpow_coef t with | true => constr:(N_of_Z t) - | _ => constr:NotConstant + | _ => constr:(NotConstant) end. Ltac Zpower_neg := diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 36863906e..fdc1288ae 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -696,7 +696,6 @@ module Make type 'a printer = { pr_tactic : tolerability -> 'tacexpr -> std_ppcmds; pr_constr : 'trm -> std_ppcmds; - pr_uconstr : 'utrm -> std_ppcmds; pr_lconstr : 'trm -> std_ppcmds; pr_dconstr : 'dtrm -> std_ppcmds; pr_pattern : 'pat -> std_ppcmds; @@ -711,7 +710,6 @@ module Make constraint 'a = < term :'trm; - utrm :'utrm; dterm :'dtrm; pattern :'pat; constant :'cst; @@ -1153,8 +1151,6 @@ module Make pr.pr_reference r | ConstrMayEval c -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c - | UConstr c -> - keyword "uconstr:" ++ pr.pr_uconstr c | TacFreshId l -> keyword "fresh" ++ pr_fresh_ids l | TacPretype c -> @@ -1182,7 +1178,6 @@ module Make let pr = { pr_tactic = pr_raw_tactic_level; pr_constr = pr_constr_expr; - pr_uconstr = pr_constr_expr; pr_dconstr = pr_constr_expr; pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; @@ -1213,7 +1208,6 @@ module Make let pr = { pr_tactic = prtac; pr_constr = pr_and_constr_expr (pr_glob_constr_env env); - pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env); pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); @@ -1255,7 +1249,6 @@ module Make let pr = { pr_tactic = pr_glob_tactic_level env; pr_constr = pr_constr_env env Evd.empty; - pr_uconstr = pr_closed_glob_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; pr_pattern = pr_constr_pattern_env env Evd.empty; diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 74d98176a..7da6df717 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -19,6 +19,8 @@ open Sigma.Notations DECLARE PLUGIN "coretactics" +(** Basic tactics *) + TACTIC EXTEND reflexivity [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 8f336cdb3..98868e8f9 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -17,6 +17,25 @@ open Tacinterp open Misctypes open Locus +(** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *) + +let create_generic_quotation name e wit = + let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in + Egramcoq.create_ltac_quotation name inject (e, None) + +let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int +let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string + +let () = create_generic_quotation "ident" Pcoq.Prim.ident Constrarg.wit_ident +let () = create_generic_quotation "reference" Pcoq.Prim.reference Constrarg.wit_ref +let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr +let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr +let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern +let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr +let () = + let inject (loc, v) = Tacexpr.Tacexp v in + Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5) + (* Rewriting orientation *) let _ = Metasyntax.add_token_obj "<-" diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index a069fd755..89dc843cb 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -651,7 +651,7 @@ and intern_tactic_as_arg loc onlytac ist a = | TacCall _ | Reference _ | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a - | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> + | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> if onlytac then error_tactic_expected loc else TacArg (loc,a) and intern_tactic_or_tacarg ist = intern_tactic false ist @@ -665,7 +665,6 @@ and intern_tactic_fun ist (var,body) = and intern_tacarg strict onlytac ist = function | Reference r -> intern_non_tactic_reference strict ist r | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) - | UConstr c -> UConstr (intern_constr ist c) | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f | TacCall (loc,f,l) -> TacCall (loc, diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1a8a95158..bf5f9ddc8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1365,11 +1365,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t = let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) end } - | UConstr c -> - Ftactic.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - Ftactic.return (Value.of_uconstr (interp_uconstr ist env c)) - end } | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist r | TacCall (loc,f,l) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 3f103a290..55941c1ca 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -247,7 +247,6 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) and subst_tacarg subst = function | Reference r -> Reference (subst_reference subst r) | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) - | UConstr c -> UConstr (subst_glob_constr subst c) | TacCall (_loc,f,l) -> TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) | TacFreshId _ as x -> x diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index aad0bb44d..8dadc2419 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -65,7 +65,7 @@ Module NonPrim. set (fibermap := fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0)). Set Printing Implicit. - let G := match goal with |- ?G => constr:G end in + let G := match goal with |- ?G => constr:(G) end in first [ match goal with | [ |- (@isconnected_elim n (@hfiber A B f (f a)) (@isconnected_hfiber_conn_map n A B f H (f a)) @@ -142,7 +142,7 @@ Module Prim. set (fibermap := fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0)). Set Printing Implicit. - let G := match goal with |- ?G => constr:G end in + let G := match goal with |- ?G => constr:(G) end in first [ match goal with | [ |- (@isconnected_elim n (@hfiber A B f (f a)) (@isconnected_hfiber_conn_map n A B f H (f a)) diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index 070d1e9c7..a327bbf2a 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -23,7 +23,7 @@ Proof. pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H (fun b => ap g (eisretr f b))) as k. revert k. - let x := match goal with |- let k := ?x in _ => constr:x end in + let x := match goal with |- let k := ?x in _ => constr:(x) end in intro k; clear k; pose (x _). pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _ diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v index 52dae265b..04fa59075 100644 --- a/test-suite/complexity/ring2.v +++ b/test-suite/complexity/ring2.v @@ -39,7 +39,7 @@ Admitted. Ltac Zcst t := match isZcst t with true => t - | _ => constr:NotConstant + | _ => constr:(NotConstant) end. Add Ring Zr : Zth diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v index 7069bba43..8462d3627 100644 --- a/test-suite/success/MatchFail.v +++ b/test-suite/success/MatchFail.v @@ -9,14 +9,14 @@ Require Export ZArithRing. Ltac compute_POS := match goal with | |- context [(Zpos (xI ?X1))] => - let v := constr:X1 in - match constr:v with + let v := constr:(X1) in + match constr:(v) with | 1%positive => fail 1 | _ => rewrite (BinInt.Pos2Z.inj_xI v) end | |- context [(Zpos (xO ?X1))] => - let v := constr:X1 in - match constr:v with + let v := constr:(X1) in + match constr:(v) with | 1%positive => fail 1 | _ => rewrite (BinInt.Pos2Z.inj_xO v) end diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 6c4d4ae98..ce9099059 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -15,7 +15,7 @@ Ltac F x := idtac; G x with G y := idtac; F y. (* Check that Match Context keeps a closure *) -Ltac U := let a := constr:I in +Ltac U := let a := constr:(I) in match goal with | |- _ => apply a end. @@ -75,7 +75,7 @@ Qed. (* Check context binding *) Ltac sym t := - match constr:t with + match constr:(t) with | context C[(?X1 = ?X2)] => context C [X1 = X2] end. @@ -143,7 +143,7 @@ Qed. Ltac check_binding y := cut ((fun y => y) = S). Goal True. -check_binding ipattern:H. +check_binding ipattern:(H). Abort. (* Check that variables explicitly parsed as ltac variables are not @@ -151,7 +151,7 @@ Abort. Ltac afi tac := intros; tac. Goal 1 = 2. -afi ltac:auto. +afi ltac:(auto). Abort. (* Tactic Notation avec listes *) @@ -174,7 +174,7 @@ Abort. empty args *) Goal True. -match constr:@None with @None => exact I end. +match constr:(@None) with @None => exact I end. Abort. (* Check second-order pattern unification *) @@ -218,7 +218,7 @@ Ltac Z1 t := set (x:=t). Ltac Z2 t := t. Goal True -> True. Z1 O. -Z2 ltac:O. +Z2 ltac:(O). exact I. Qed. @@ -302,7 +302,7 @@ Abort. (* Check instantiation of binders using ltac names *) Goal True. -let x := ipattern:y in assert (forall x y, x = y + 0). +let x := ipattern:(y) in assert (forall x y, x = y + 0). intro. destruct y. (* Check that the name is y here *) Abort. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index c41eb2fa2..627a1a495 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -452,7 +452,7 @@ Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; - [(do_partial_apps H m' ltac:idtac)|clear H] + [(do_partial_apps H m' ltac:(idtac))|clear H] | _ => cont end in diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 8d942d908..81b31d783 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -465,7 +465,7 @@ Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; - [(do_partial_apps H m' ltac:idtac)|clear H] + [(do_partial_apps H m' ltac:(idtac))|clear H] | _ => cont end in diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 145d451f0..190397ae4 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -77,23 +77,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic3(t) := - setoidreplace (default_relation x y) ltac:t. + setoidreplace (default_relation x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (default_relation x y) ltac:t o. + setoidreplaceat (default_relation x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (default_relation x y) id ltac:t. + setoidreplacein (default_relation x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (default_relation x y) id ltac:t o. + setoidreplaceinat (default_relation x y) id ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) := @@ -107,13 +107,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "by" tactic3(t) := - setoidreplace (rel x y) ltac:t. + setoidreplace (rel x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (rel x y) ltac:t o. + setoidreplaceat (rel x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) @@ -130,14 +130,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (rel x y) id ltac:t. + setoidreplacein (rel x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (rel x y) id ltac:t o. + setoidreplaceinat (rel x y) id ltac:(t) o. (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back to the user to discharge the diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index 215b8bd58..d160f5f1d 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -19,13 +19,13 @@ Local Open Scope list_scope. Ltac isInt31cst_lst l := match l with - | nil => constr:true + | nil => constr:(true) | ?t::?l => match t with | D1 => isInt31cst_lst l | D0 => isInt31cst_lst l - | _ => constr:false + | _ => constr:(false) end - | _ => constr:false + | _ => constr:(false) end. Ltac isInt31cst t := @@ -38,17 +38,17 @@ Ltac isInt31cst t := ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20 ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil) in isInt31cst_lst l - | Int31.On => constr:true - | Int31.In => constr:true - | Int31.Tn => constr:true - | Int31.Twon => constr:true - | _ => constr:false + | Int31.On => constr:(true) + | Int31.In => constr:(true) + | Int31.Tn => constr:(true) + | Int31.Twon => constr:(true) + | _ => constr:(false) end. Ltac Int31cst t := match isInt31cst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** The generic ring structure inferred from the Cyclic structure *) diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index ec495d094..56cb9bbc2 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -148,26 +148,26 @@ Ltac isBigZcst t := match t with | BigZ.Pos ?t => isBigNcst t | BigZ.Neg ?t => isBigNcst t - | BigZ.zero => constr:true - | BigZ.one => constr:true - | BigZ.two => constr:true - | BigZ.minus_one => constr:true - | _ => constr:false + | BigZ.zero => constr:(true) + | BigZ.one => constr:(true) + | BigZ.two => constr:(true) + | BigZ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigZcst t := match isBigZcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigZ_to_N t := match t with | BigZ.Pos ?t => BigN_to_N t - | BigZ.zero => constr:0%N - | BigZ.one => constr:1%N - | BigZ.two => constr:2%N - | _ => constr:NotConstant + | BigZ.zero => constr:(0%N) + | BigZ.one => constr:(1%N) + | BigZ.two => constr:(2%N) + | _ => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 29a1145e0..ec1017f50 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -119,10 +119,10 @@ Qed. Ltac isStaticWordCst t := match t with - | W0 => constr:true + | W0 => constr:(true) | WW ?t1 ?t2 => match isStaticWordCst t1 with - | false => constr:false + | false => constr:(false) | true => isStaticWordCst t2 end | _ => isInt31cst t @@ -139,30 +139,30 @@ Ltac isBigNcst t := | BigN.N6 ?t => isStaticWordCst t | BigN.Nn ?n ?t => match isnatcst n with | true => isStaticWordCst t - | false => constr:false + | false => constr:(false) end - | BigN.zero => constr:true - | BigN.one => constr:true - | BigN.two => constr:true - | _ => constr:false + | BigN.zero => constr:(true) + | BigN.one => constr:(true) + | BigN.two => constr:(true) + | _ => constr:(false) end. Ltac BigNcst t := match isBigNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigN_to_N t := match isBigNcst t with | true => eval vm_compute in (BigN.to_N t) - | false => constr:NotConstant + | false => constr:(NotConstant) end. Ltac Ncst t := match isNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index fe38ea4f2..850afe534 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -104,18 +104,18 @@ Ltac isBigQcst t := | BigQ.Qz ?t => isBigZcst t | BigQ.Qq ?n ?d => match isBigZcst n with | true => isBigNcst d - | false => constr:false + | false => constr:(false) end - | BigQ.zero => constr:true - | BigQ.one => constr:true - | BigQ.minus_one => constr:true - | _ => constr:false + | BigQ.zero => constr:(true) + | BigQ.one => constr:(true) + | BigQ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigQcst t := match isBigQcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Add Field BigQfield : BigQfieldth diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 27e1ca844..17f05c511 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -238,8 +238,8 @@ Ltac inject_left H := Ltac inject_right H := progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H. -Ltac autoinjections_left := repeat autoinjection ltac:inject_left. -Ltac autoinjections_right := repeat autoinjection ltac:inject_right. +Ltac autoinjections_left := repeat autoinjection ltac:(inject_left). +Ltac autoinjections_right := repeat autoinjection ltac:(inject_right). Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 66ca3e577..7384790da 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -252,7 +252,7 @@ Ltac autoinjection tac := Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H. -Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject). +Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:(inject)). (** Destruct an hypothesis by first copying it to avoid dependencies. *) diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index 2465f0399..e57af7311 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -35,7 +35,7 @@ Qed. (**********) Ltac intro_hyp_glob trm := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => match goal with | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 @@ -55,7 +55,7 @@ Ltac intro_hyp_glob trm := | _ => idtac end | (?X1 / ?X2)%F => - let aux := constr:X2 in + let aux := constr:(X2) in match goal with | _:(forall x0:R, aux x0 <> 0) |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 @@ -82,7 +82,7 @@ Ltac intro_hyp_glob trm := | _ => idtac end | (/ ?X1)%F => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | _:(forall x0:R, aux x0 <> 0) |- (derivable _) => intro_hyp_glob X1 @@ -108,7 +108,7 @@ Ltac intro_hyp_glob trm := | (pow_fct _) => idtac | Rabs => idtac | ?X1 => - let p := constr:X1 in + let p := constr:(X1) in match goal with | _:(derivable p) |- _ => idtac | |- (derivable p) => idtac @@ -130,7 +130,7 @@ Ltac intro_hyp_glob trm := (**********) Ltac intro_hyp_pt trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => match goal with | |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt @@ -156,7 +156,7 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | (?X1 / ?X2)%F => - let aux := constr:X2 in + let aux := constr:(X2) in match goal with | _:(aux pt <> 0) |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt @@ -202,7 +202,7 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | (/ ?X1)%F => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | _:(aux pt <> 0) |- (derivable_pt _ _) => intro_hyp_pt X1 pt @@ -249,7 +249,7 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | ?X1 => - let p := constr:X1 in + let p := constr:(X1) in match goal with | _:(derivable_pt p pt) |- _ => idtac | |- (derivable_pt p pt) => idtac @@ -578,89 +578,89 @@ Ltac is_cont_glob := (**********) Ltac rew_term trm := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 + X4)) - | _ => constr:(p1 + p2)%F + | _ => constr:((p1 + p2)%F) end - | _ => constr:(p1 + p2)%F + | _ => constr:((p1 + p2)%F) end | (?X1 - ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 - X4)) - | _ => constr:(p1 - p2)%F + | _ => constr:((p1 - p2)%F) end - | _ => constr:(p1 - p2)%F + | _ => constr:((p1 - p2)%F) end | (?X1 / ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 / X4)) - | _ => constr:(p1 / p2)%F + | _ => constr:((p1 / p2)%F) end | _ => - match constr:p2 with - | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F - | _ => constr:(p1 / p2)%F + match constr:(p2) with + | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F) + | _ => constr:((p1 / p2)%F) end end | (?X1 * / ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 / X4)) - | _ => constr:(p1 / p2)%F + | _ => constr:((p1 / p2)%F) end | _ => - match constr:p2 with - | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F - | _ => constr:(p1 / p2)%F + match constr:(p2) with + | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F) + | _ => constr:((p1 / p2)%F) end end | (?X1 * ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 * X4)) - | _ => constr:(p1 * p2)%F + | _ => constr:((p1 * p2)%F) end - | _ => constr:(p1 * p2)%F + | _ => constr:((p1 * p2)%F) end | (- ?X1) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X2) => constr:(fct_cte (- X2)) - | _ => constr:(- p)%F + | _ => constr:((- p)%F) end | (/ ?X1) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X2) => constr:(fct_cte (/ X2)) - | _ => constr:(/ p)%F + | _ => constr:((/ p)%F) end - | (?X1 AppVar) => constr:X1 + | (?X1 AppVar) => constr:(X1) | (?X1 ?X2) => let p := rew_term X2 in - match constr:p with + match constr:(p) with | (fct_cte ?X3) => constr:(fct_cte (X1 X3)) | _ => constr:(comp X1 p) end - | AppVar => constr:id + | AppVar => constr:(id) | (AppVar ^ ?X1) => constr:(pow_fct X1) | (?X1 ^ ?X2) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3)) | _ => constr:(comp (pow_fct X2) p) end @@ -669,7 +669,7 @@ Ltac rew_term trm := (**********) Ltac deriv_proof trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in constr:(derivable_pt_plus X1 X2 pt p1 p2) @@ -684,14 +684,14 @@ Ltac deriv_proof trm pt := | id:(?X2 pt <> 0) |- _ => let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in constr:(derivable_pt_div X1 X2 pt p1 p2 id) - | _ => constr:False + | _ => constr:(False) end | (/ ?X1)%F => match goal with | id:(?X1 pt <> 0) |- _ => let p1 := deriv_proof X1 pt in constr:(derivable_pt_inv X1 pt p1 id) - | _ => constr:False + | _ => constr:(False) end | (comp ?X1 ?X2) => let pt_f1 := eval cbv beta in (X2 pt) in @@ -710,21 +710,21 @@ Ltac deriv_proof trm pt := | sqrt => match goal with | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id) - | _ => constr:False + | _ => constr:(False) end | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt) | ?X1 => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with - | id:(derivable_pt aux pt) |- _ => constr:id + | id:(derivable_pt aux pt) |- _ => constr:(id) | id:(derivable aux) |- _ => constr:(id pt) - | _ => constr:False + | _ => constr:(False) end end. (**********) Ltac simplify_derive trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => try rewrite derive_pt_plus; simplify_derive X1 pt; simplify_derive X2 pt @@ -753,7 +753,7 @@ Ltac simplify_derive trm pt := | Rsqr => try rewrite derive_pt_Rsqr | sqrt => try rewrite derive_pt_sqrt | ?X1 => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | id:(derive_pt aux pt ?X2 = _),H:(derivable aux) |- _ => try replace (derive_pt aux pt (H pt)) with (derive_pt aux pt X2); diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index d210792f9..32e13d389 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -225,11 +225,11 @@ Module MoreInt (Import I:Int). (** [int] to [ExprI] *) Ltac i2ei trm := - match constr:trm with - | 0 => constr:EI0 - | 1 => constr:EI1 - | 2 => constr:EI2 - | 3 => constr:EI3 + match constr:(trm) with + | 0 => constr:(EI0) + | 1 => constr:(EI1) + | 2 => constr:(EI2) + | 3 => constr:(EI3) | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey) | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey) | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey) @@ -241,7 +241,7 @@ Module MoreInt (Import I:Int). (** [Z] to [ExprZ] *) with z2ez trm := - match constr:trm with + match constr:(trm) with | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey) | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey) | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey) @@ -254,7 +254,7 @@ Module MoreInt (Import I:Int). (** [Prop] to [ExprP] *) Ltac p2ep trm := - match constr:trm with + match constr:(trm) with | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey) | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey) | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey) diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index b80eb4451..f4baba190 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -30,12 +30,12 @@ Local Open Scope Z_scope. Ltac compute_POS := match goal with | |- context [(Zpos (xI ?X1))] => - match constr:X1 with + match constr:(X1) with | context [1%positive] => fail 1 | _ => rewrite (Pos2Z.inj_xI X1) end | |- context [(Zpos (xO ?X1))] => - match constr:X1 with + match constr:(X1) with | context [1%positive] => fail 1 | _ => rewrite (Pos2Z.inj_xO X1) end |